Finishing a review as a non-maintainer?

Stream: mathlib4

[Thomas Murrills]

I've occasionally seen "maintainer merge" being commented at the end of reviewed PR's—is that the right way to finish off a review as a non-maintainer? What does that do? Or is a simple "LGTM!" all that's necessary?

[Jireh Loreaux]

LGTM is all that's necessary. maintainer merge is for people listed as "mathlib reviewers" (the list is on the website). When they add that string then it pings all the maintainers in a Zulip thread to take a look (the bot says it has been placed on the "maintainer queue"). If you write that without that reviewer status it doesn't have the same effect.

[Jireh Loreaux]

If you wanted to do a bit more to indicate you're happy with it, you could post in the PR review stream (are you subscribed to that stream?) in a new topic with the PR number in the subject. You could explain what the PR does and why you're happy with it. That being said, none of that is necessary, a simple LGTM on GitHub is fine too.

[Thomas Murrills]

I see, thanks!