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