Luís Oliveira luismbo@gmail.com writes:
The first option is clearly the easiest since all you have to do is click GitHub's merge button, but I personally find that the merge commits pollute the history (particularly if only one or two commits are being merged). I know João disagrees with me on this matter.
I don't think of merge commit objects as pollution. At least in the particular "Merge-button" workflow, in other cases it is indeed problematic, but these are not relevant here.
The "merge" button also has these advantages:
* it is very familiar in the github ecosystem, and github passers-by will find it familiar (as they already have apparently).
* It makes for a very pretty and readable "network" graph
https://github.com/slime/slime/network
* It makes the history on https://github.com/slime/slime/commits/master accurately reflect the pull requests merged, and link to their respective discussion threads.
I've confirmed that I when tried out Luís's rebase technique for https://github.com/slime/slime/pull/73, we didn't get the last two advantages. Plus, as Luís says, it is more complicated for git newbies, and requires a separate step to close the pull request.
So yes, I'm partial to the first, but won't kill myself over it, particularly for small changes as you say. For big changes I might cut a wrist or two :-)
João