On Sat 29 Dec 2018 at 18:19, Stephen Connolly < stephen.alan.conno...@gmail.com> wrote:
> > > On Sat 29 Dec 2018 at 18:06, Vladimir Sitnikov < > sitnikov.vladi...@gmail.com> wrote: > >> Stephen> Nah. Once committers have approved the PR then the PR can be >> merged by the >> Stephen> creator of the PR even if not a committer... at least that’s >> the default >> Stephen> way GitHub PRs work >> >> By default one needs push rights on the repository to merge PRs. >> "Approval" changes nothing. "PR approval" does not differ from any >> other comment. >> In other words, non-committers can't merge PRs. > > > Well on other GitHub orgs i’ve seen PR author has Merge button once PR is > approved by someone with push rights to the repo... until they add a commit > or the merge result changes > Gitbox may be configuring synchronised repos differently, but for interop with the rest of GitHub we shouldn’t assume approval of a PR by committers will not enable self-merging >> >> Vladimir >> >> --------------------------------------------------------------------- >> To unsubscribe, e-mail: dev-unsubscr...@maven.apache.org >> For additional commands, e-mail: dev-h...@maven.apache.org >> >> -- > Sent from my phone > -- Sent from my phone
