Skip to content

Fix duplicate egui id in the stream trees #16413

Fix duplicate egui id in the stream trees

Fix duplicate egui id in the stream trees #16413

Workflow file for this run

name: "Approve Workflow Runs"
on:
pull_request_target:
issue_comment:
types: [created, edited]
defaults:
run:
shell: bash
permissions:
contents: "read"
actions: "write"
jobs:
approve-workflow-runs:
name: "Check for approval"
runs-on: ubuntu-latest
if: |
github.event.pull_request.head.repo.owner.login != 'rerun-io' &&
(github.event_name == 'pull_request_target' || github.event.issue.pull_request)
steps:
- name: Checkout
uses: actions/checkout@v4
- uses: prefix-dev/setup-pixi@v0.8.1
with:
pixi-version: v0.34.0
- name: Wait a few seconds
run: |
# Give GitHub a bit of time to synchronize everything
sleep 5s
- name: Approve workflow runs
run: |
pixi run python scripts/ci/approve_workflow_runs.py \
--github-token "${{ secrets.GITHUB_TOKEN }}" \
--github-repository "rerun-io/rerun" \
--pr-number "${{ github.event.pull_request.number || github.event.issue.number }}"