On Wed, Oct 25, 2017 at 2:17 PM, Vinnie Falco via Boost < boost@lists.boost.org> wrote:
On Wed, Oct 25, 2017 at 11:03 AM, Fernando Cacciola via Boost
wrote: but even though I'm logged with my Github account, it appears I don't have write-access to merge this PR.
I'm not a fan of using the GitHub web interface to merge pull requests because this needlessly creates a "merge commit" (usually with one side of the merge having just one commit) which interferes with a linear history (I prefer a linear history except for when there are two ongoing topical branches that are merged at some point).
Vinnie, have you tried using the "Rebase and Merge" option in github? It eliminates the merge, but it does make a new commit ID. If you're not working on a commit pipeline, this option will make things a bit easier. - Jim