On 07/04/18 21:37, Vinnie Falco via Boost wrote:
On Wed, Jul 4, 2018 at 6:33 PM, James E. King III
wrote: I don't have appropriate privileges to boostorg/website to merge anything, so it won't happen that way. So sad. I was half-joking, but you don't need privileges to retrieve the branches locally, merge them into a new local branch, push the local branch to your remote fork (GitHub), and then submit the branch on the remote fork as a pull request. The miracle of Git!
While I appreciate the work to resolve conflicts by "merging" multiple PRs into one, it still feels odd to suggest to inject another task into the pipeline. Wouldn't it be simpler if someone *with* commit privileges would take on the task to do the merging at once ? (And yes, if no-one who already has such privileges is willing or has time to do this, I'd sign up for the job.) Regards, Stefan -- ...ich hab' noch einen Koffer in Berlin...