Skip to content

[Merged by Bors] - chore(Data/Finsupp): split off basic scalar multiplication #48572

[Merged by Bors] - chore(Data/Finsupp): split off basic scalar multiplication

[Merged by Bors] - chore(Data/Finsupp): split off basic scalar multiplication #48572

# This workflow allows any user to add one of the `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 && (contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
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 awaitingAuthor = commentLines.includes('awaiting-author');
const wip = commentLines.includes('WIP');
if (awaitingAuthor || wip) {
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 (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'] });
}