chore: run CI on new labels (#3003)

CI will now run on _any_ manually added label; hard to avoid. Fun fact: Because the `toolchain-available` label is added by a github action with the default token, it will _not_ trigger the workflow. Lucky coincidence.
leanprover · Dec 1, 2023 · a5af90c · a5af90c
1 parent 5937f42
commit a5af90c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -6,6 +6,7 @@ on:
     tags:
       - '*'
   pull_request:
+    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT