heartbeat: allow muting a heartbeat monitor #2785
This file contains 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: labeler | |
| on: | |
| pull_request_target: | |
| types: ['opened', 'ready_for_review', 'reopened', 'synchronize'] | |
| jobs: | |
| labeler: | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| runs-on: ubuntu-latest | |
| if: github.event.pull_request.draft == false | |
| name: Label the PR size | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: # checkout the base branch, where we run the script from | |
| path: base | |
| - uses: actions/checkout@v4 | |
| with: # checkout the merge commit, where the PR changes are | |
| ref: refs/pull/${{ github.event.number }}/merge | |
| path: merge | |
| # we need full history | |
| fetch-depth: 0 | |
| - name: Run labeler script from base | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_NUMBER: ${{ github.event.number }} | |
| FAIL_IF_XL: '1' | |
| MAIN_BRANCH: ${{ github.event.pull_request.base.ref }} | |
| run: cd merge && ../base/devtools/scripts/github-set-pr-label.sh |