How about the documentation? Is there something I haven't seen yet? The Contributing.md file just says that it exists. Not that merge-pr.sh would have documentation, but I know what it does.
Merge PR is still useful for backports and other stuff that the bot doesn't handle I think ; also, I don't like to depend on the bot without a fallback
@Michael Soegtrop coqbot does not have warnings: it refuses to merge in some cases (no assignee, no kind label, left-over needs label, no milestone, author merge their own PR) but it doesn't check the status of CI (it assumes that the merger did it since it's right in front of their nose).
However, @Gaëtan Gilbert we shouldn't remove the merge script because it's still needed to merge in release branches (coqbot doesn't do that yet).
We could add a warning to the merge script saying: you are merging in master, why don't you use the bot.
@Théo Zimmermann : thanks! I think this information should go here:(https://github.com/coq/coq/blob/master/CONTRIBUTING.md#additional-notes-for-pull-request-reviewers-and-assignees). I will give coqbot a try next time.
@Michael Soegtrop Can you open a PR with the additional info you'd like to see, or open an issue and assign me to it?
@Théo Zimmermann : I will draft something and you correct it in case.
@Théo Zimmermann : i am just doing the PR. One question: reviewers are allowed to do minor changes to a PR and still merge themselves according to the rules (afaik). Can you elaborate on what coqbot actually checks? Say just the main author? Are minor corrections by reviewers still possible?
Yes, coqbot does a very dumb check: it looks at the author of the PR according to GitHub, not according to the commit it contains.
Last updated: Oct 21 2021 at 21:03 UTC