Subject: Re: [boost] Release notes piling up
From: Stefan Seefeld (stefan_at_[hidden])
Date: 2018-07-05 01:46:36
On 07/04/18 21:37, Vinnie Falco via Boost wrote:
> On Wed, Jul 4, 2018 at 6:33 PM, James E. King III <jking_at_[hidden]> 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.)
-- ...ich hab' noch einen Koffer in Berlin...