[m-rev.] Handling pull requests

[Peter Wang]

Hi,

The simplest way I've seen to handle pull requests is to apply like
this:  (the url was given in the notification message)

    curl https://github.com/Mercury-Language/mercury/pull/1.patch | git am -3

You may want to amend the commits before pushing.

For bigger changes you can create a local branch from a pull request,
then go from there, e.g. to create `pr3' from pull request #3:

    git fetch origin pull/3/head:pr3

I suggest that we try to keep the history linear and avoid pointless
merge commits, by rebasing the changes onto the latest master before
pushing.

Peter