mathlib
79a2eb39 - chore(.github/workflows): `maintainer merge` workflow (#16555)

Commit
3 years ago
chore(.github/workflows): `maintainer merge` workflow (#16555) This PR adds a workflow that will listen for PR comments containing the phrase `maintainer merge` at the beginning of a line. It is intended for use by mathlib reviewers to flag to mathlib maintainers that they have reviewed a PR and consider it ready for merging. - The workflow will send a message to the maintainer stream on zulip to ping maintainers. - The workflow will add a comment confirming that the ping has been sent. - The workflow will only work for messages from members of the "mathlib reviewers" team in the leanprover-community organization. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading