Be more lax on what merged PRs we detect, but post an alert.

[Zimmi48]

It happens more often than I expected that maintainers use the merge button, even though it's explicitly forbidden in the merging rules. Examples by different maintainers:

• 8.14: warn deprecated locality on Instance even when interactive rocq#15243
• [stdlib] Add changelog for PR #11335 rocq#11993
• Fix #11552: Ltac2 breaks query commands during proofs. rocq#11629
• Annotate Ltac2 match macro variables with their type. rocq#11605
• Move plugin tutorial to Coq repo rocq#8778

Therefore, it can happen that we miss PRs for which backporting would have been required. This is what has happened in the case of rocq-prover/rocq#11629, where the backporting process was handled manually.

This PR detects these offending PRs, but as is it is incomplete because in cases where we merge subtrees coming from other repositories, such as in the case of rocq-prover/rocq#8778, we might get confused by a bunch of merge commits that are not from the Coq repository. We can think of various ways to solve this issue.

In case we notice a wrong merge commit message, we could alert the maintainer that they are not following the documentation. Currently, all the code does is to put a warning in the log.

[Zimmi48]

This more lax criterion was implemented in 22ea1a8, as part of #305, but without posting any alert, and without the careful considerations for the case of merging subtrees. So we might want to revisit this.