pr got approved, but not merged. bot does nothing

[davidak]

the bot should do something to get the pr merged

NixOS/nixpkgs#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]

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]

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.