search

timokau / marvin-mk2

Discontinued! See https://github.com/timokau/marvin-mk2/issues/34#issuecomment-1100656280 (Previously: "Making sure your PR gets a review and your reviews don't get lost.")
https://github.com/apps/marvin-mk2
MIT License
19 stars 9 forks source link

pr got approved, but not merged. bot does nothing #84

Open davidak opened 4 years ago

davidak commented 4 years ago

the bot should do something to get the pr merged

https://github.com/NixOS/nixpkgs/pull/77009

the bot could set /status needs_merger, when a reviewer has no commit rights and approved

maybe there should be a rule that a pr should have at least 2 approvals before it can get merged, so an impactful pr get's not merged by the first reviewer

timokau commented 4 years ago

It seems like there might be a misunderstanding, this bot will never merge anything itself. It will only label a PR as needing merge and maybe request a review from someone with the right permission.

Its an intentional choice to require an explicit /status needs_merge instead of reacting to GitHub approvals. That is because GH approvals have a bit of a vague meaning and are used by different people for different purposes. I'm not yet 100% sure if we want to keep it that way, maybe once the bot is more established people would know what an "approval" means. Another alternative is to write a message when someone approves but does not set to needs_merge that explains the situation.

davidak commented 4 years ago

Thanks for the explanation!

Another alternative is to write a message when someone approves but does not set to needs_merge that explains the situation.

Yes, that would help, so the PR is not stuck again with reviews, but no merge.

-- Diese Nachricht wurde von meinem Android-Gerät mit K-9 Mail gesendet.