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

Zimmi48 wants to merge 1 commit intorocq-prover:masterrocq-prover/bot:masterfrom

Zimmi48:merged-with-buttonZimmi48/bot:merged-with-buttonCopy head branch name to clipboard