Maintainer merge (review) #16688

	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/[email protected]
	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: '[email protected]'
	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/[email protected]
	with:
	issue-number: ${{ github.event.pull_request.number }}
	body: \|
	🚀 Pull request has been placed on the maintainer queue by ${{ github.event.review.user.login }}.

Provide feedback