GitHub workflow for the SLIME repo

[Luís Oliveira]

One thing we should agree on is how to merge pull requests. This blog
post presents the three alternatives:
<http://differential.io/blog/best-way-to-merge-a-github-pull-request>.

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.

It's pretty easy to implement the other workflows with a couple of
commands, something like:

  # see <https://help.github.com/articles/checking-out-pull-requests-locally>
  # on an up-to-date repo
  $ git checkout pr/66
  $ git rebase origin/master
  $ git push origin pr/66:master

Or using hub (<http://hub.github.com>):

  # on an up-to-date master
  $ hub am https://github.com/slime/slime/pull/66
  $ git push

I'm partial to the second option listed on the blog post, but I have
very few commits in SLIME so my opinion should weight very little. :-)

Cheers,

-- 
Luís Oliveira
http://kerno.org/~luis/