Hey Geertjan, Am Freitag, den 06.10.2017, 19:44 +0200 schrieb Geertjan Wielenga: > Another question -- once we have reviewed a PR, and there's consensus on > it, how do we do the merge?
if the PR that should be merged was your own, you can do this: * git checkout master * git pull (assuming you configured master to track upstream master) * git merge <branch_backing_your_PR> * git push upstream (assuming the apache repository is configure as upstream) github and/or the apache gitbot recognise, that the merged commit/commits are identical to the PR and close that PR automaticly. To make it easy to merge PRs from github, I followed this link, that was already posted: https://cwiki.apache.org/confluence/display/ROLLER/How+to+accept+a+GitHub+Pull+Request This is pretty comprehensive. HTH Matthias
