Subject: Re: [boost] Seems like I need write-access to merge a PR
From: Vinnie Falco (vinnie.falco_at_[hidden])
Date: 2017-10-25 19:03:20
On Wed, Oct 25, 2017 at 11:29 AM, Stefan Seefeld via Boost
> That is no longer true (and hasn't for quite a while). Nowadays the web
> interface allows you to select different PR merge methods, including the
> traditional merge commit, a "squash and merge", or a "rebase and merge".
> It sounds like what you'd prefer is the latter, to make the history linear.
I do like the linear history where practical but that is not the only
reason to avoid using the GitHub interface.
Assembling the branch locally has an additional benefit. You can
preview exactly how the branch will look after the merge. This is not
possible with the GitHub interface. You also cannot sign commits with
the GitHub interface or make adjustments. Everyone who has ever
submitted a pull request always forgets to update CHANGELOG.md.
Furthermore I have a policy in my repository that the tip of the
master and develop branches that the top commit always sets an
internal version number. Merging a pull request won't accomplish that.
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk