feat: add toolchain-available labels to PRs (#2492)

This commit is contained in:
Scott Morrison 2023-08-31 18:36:32 +10:00 committed by GitHub
parent 7de335c661
commit b2119313bd
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -70,6 +70,13 @@ jobs:
# The token used here must have `workflow` privileges.
GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
- name: Add label
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: actions-ecosystem/action-add-labels@v1
with:
number: ${{ steps.workflow-info.outputs.pullRequestNumber }}
labels: toolchain-available
# We next automatically create a Mathlib branch using this toolchain.
# Mathlib CI will be responsible for reporting back success or failure
# to the PR comments asynchronously.