Skip to content

Maintainer merge (review) #7705

Maintainer merge (review)

Maintainer merge (review) #7705

name: Maintainer merge (review)
on:
pull_request_review:
types: [submitted, edited]
jobs:
ping_zulip:
name: Ping maintainers on Zulip
if: (startsWith(github.event.review.body, 'maintainer merge') || contains(toJSON(github.event.review.body), '\r\nmaintainer merge'))
runs-on: ubuntu-latest
steps:
- name: Check whether user is part of mathlib-reviewers team
uses: TheModdingInquisition/actions-team-membership@v1.0
with:
organization: 'leanprover-community'
team: 'mathlib-reviewers' # required. The team to check for
token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
- name: Send message on Zulip
uses: zulip/github-actions-zulip/send-message@v1
with:
api-key: ${{ secrets.ZULIP_API_KEY }}
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
organization-url: 'https://leanprover.zulipchat.com'
to: 'mathlib reviewers'
type: 'stream'
topic: 'maintainer merge'
content: |
${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.review.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
> ${{ github.event.pull_request.title }}
- name: Add comment to PR
uses: GrantBirki/comment@v2.0.1
with:
issue-number: ${{ github.event.pull_request.number }}
body: |
🚀 Pull request has been placed on the maintainer queue by ${{ github.event.review.user.login }}.