chore: upstream Nat.binaryRec
#1466
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
| # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels, | |
| # by commenting on the PR or issue. | |
| # Other labels from this set are removed automatically at the same time. | |
| name: Label PR based on Comment | |
| on: | |
| issue_comment: | |
| types: [created] | |
| jobs: | |
| update-label: | |
| if: github.event.issue.pull_request != null && (github.event.comment.body == 'awaiting-review' || github.event.comment.body == 'awaiting-author' || github.event.comment.body == 'WIP') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Remove all relevant labels | |
| uses: actions/github-script@v6 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| script: | | |
| const { owner, repo, number: issue_number } = context.issue; | |
| // Remove the labels if they exist | |
| await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {}); | |
| await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-author' }).catch(() => {}); | |
| await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'WIP' }).catch(() => {}); | |
| - name: Add label based on comment | |
| uses: actions/github-script@v6 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| script: | | |
| const { owner, repo, number: issue_number } = context.issue; | |
| const commentBody = context.payload.comment.body; | |
| if (commentBody == 'awaiting-review') { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-review'] }); | |
| } else if (commentBody == 'awaiting-author') { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-author'] }); | |
| } else if (commentBody == 'WIP') { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] }); | |
| } | |
| # - name: Delete the comment | |
| # uses: actions/github-script@v6 | |
| # with: | |
| # github-token: ${{ secrets.GITHUB_TOKEN }} | |
| # script: | | |
| # const { owner, repo } = context.repo; | |
| # await github.rest.issues.deleteComment({ owner, repo, comment_id: context.payload.comment.id }); |