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 > > > Vladimir > > --------------------------------------------------------------------- > To unsubscribe, e-mail: dev-unsubscr...@maven.apache.org > For additional commands, e-mail: dev-h...@maven.apache.org > > -- Sent from my phone
