ci: Don't run user code when autolabelling (#35153) #21527
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: continuous integration (staging) | |
| on: | |
| push: | |
| branches: | |
| - staging | |
| - trying | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }} | |
| # cancel any running workflow with the same label | |
| cancel-in-progress: true | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read | |
| pull-requests: write # Only allow PR comments/labels | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| build: | |
| name: ci (staging) | |
| if: ${{ github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' }} | |
| uses: ./.github/workflows/build_template.yml | |
| with: | |
| concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }} | |
| pr_branch_ref: ${{ github.sha }} | |
| # We don't wan't 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs | |
| runs_on: ${{ github.ref_name == 'trying' && 'pr' || 'bors' }} | |
| secrets: inherit |