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
On Wed, Oct 25, 2017 at 11:03 AM, Fernando Cacciola via Boost
wrote: linear history (I prefer a linear history except for when there are two ongoing topical branches that are merged at some point). 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
On 25.10.2017 14:17, Vinnie Falco via Boost wrote: 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. FWIW, Stefan -- ...ich hab' noch einen Koffer in Berlin...