Merging pull requests before 72 hours

[Leonardo Brondani Schenkel]

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.