Re: Process for handling GitHub PRs and closing them

2017-06-19 Thread Matt Sicker
What I've done on other Apache projects is essentially "git pull github/pull/N/head", merging directly into master (this is after it's ready to merge of course). After pushing that, GitHub will see that the branch is merged and auto-closes the PR. If you rewrite history as with the rebase example,

Re: Process for handling GitHub PRs and closing them

2017-06-19 Thread Jaikiran Pai
On 19-Jun-2017, at 2:43 PM, Nicolas Lalevée wrote: > >> Le 19 juin 2017 à 05:14, Jaikiran Pai a écrit : >> >> We have (read only) github repos which back our main ASF git repos (consider >> the github ant-ivy repo which is a read-only

Re: Process for handling GitHub PRs and closing them

2017-06-19 Thread Nicolas Lalevée
> Le 19 juin 2017 à 05:14, Jaikiran Pai a écrit : > > We have (read only) github repos which back our main ASF git repos (consider > the github ant-ivy repo which is a read-only mirror of ASF git repo). Users > submit pull requests to our github repos and the process

Re: Process for handling GitHub PRs and closing them

2017-06-19 Thread Stefan Bodewig
On 2017-06-19, Jaikiran Pai wrote: > We have (read only) github repos which back our main ASF git repos > (consider the github ant-ivy repo which is a read-only mirror of ASF > git repo). Users submit pull requests to our github repos and the > process I follow for merging such PRs is the