feat: HashMap.toList_map_fst #8447
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`, `WIP`, | |
| # `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue. | |
| # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels | |
| # from that set are removed automatically at the same time. | |
| # Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed. | |
| name: Label PR based on Comment | |
| on: | |
| issue_comment: | |
| types: [created] | |
| jobs: | |
| update-label: | |
| if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-')) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Add label based on comment | |
| uses: actions/github-script@v7 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| script: | | |
| const { owner, repo, number: issue_number } = context.issue; | |
| const commentLines = context.payload.comment.body.split('\r\n'); | |
| const awaitingReview = commentLines.includes('awaiting-review'); | |
| const awaitingAuthor = commentLines.includes('awaiting-author'); | |
| const wip = commentLines.includes('WIP'); | |
| const releaseCI = commentLines.includes('release-ci'); | |
| const changelogMatch = commentLines.find(line => line.startsWith('changelog-')); | |
| if (awaitingReview || awaitingAuthor || wip) { | |
| 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(() => {}); | |
| } | |
| if (awaitingReview) { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-review'] }); | |
| } | |
| if (awaitingAuthor) { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-author'] }); | |
| } | |
| if (wip) { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] }); | |
| } | |
| if (releaseCI) { | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] }); | |
| } | |
| if (changelogMatch) { | |
| const changelogLabel = changelogMatch.trim(); | |
| const { data: existingLabels } = await github.rest.issues.listLabelsOnIssue({ owner, repo, issue_number }); | |
| const changelogLabels = existingLabels.filter(label => label.name.startsWith('changelog-')); | |
| // Remove all other changelog labels | |
| for (const label of changelogLabels) { | |
| if (label.name !== changelogLabel) { | |
| await github.rest.issues.removeLabel({ owner, repo, issue_number, name: label.name }).catch(() => {}); | |
| } | |
| } | |
| // Add the new changelog label | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [changelogLabel] }); | |
| } |