My two cents:
I'm a committer, and if I'm doing a trivial bump of an openmaintainer
port I'll push it directly. If I'm opening a GitHub PR for an
openmaintainer port this means that for some reason I want the
maintainer's opinion/review before it gets merged.
As a maintainer, I would be annoyed if I was notified of a PR and at the
time I look into it (within the 72-hour period) it was already merged.
My belief is that in general nobody else should merge the PRs besides
the submitter of the PR and/or the maintainer. They can merge at any
time of their choosing in case they want to proceed, and there is no
need to second guess their intentions. A third-party just needs to
intervene on maintainer timeouts or when neither participant is a
committer. And if a third-party always asks the participants for
confirmation before unilaterally merging, there's little room for
misunderstandings.
So I'm with Ryan and Mojca on this one.
// Leonardo.
