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

Draft

Zimmi48 wants to merge 1 commit intocoq:masterfrom Zimmi48:merged-with-button

+18-3

Commits on Dec 17, 2021

Be more lax on what merged PRs we detect, warn in log.
Zimmi48
committed