mathlib3
61cd266a - ci(.github/workflows): automatically remove awaiting-CI label (#9491)

Commit
4 years ago
ci(.github/workflows): automatically remove awaiting-CI label (#9491) This PR adds a job to our CI which removes the label "awaiting-CI" when the build finishes successfully. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/awaiting-CI.2C.20.23bors.2C.20and.20the.20PR.20.23queue/near/255754196)
Parents
Loading