I got a notification email for a Pull Request on GitHub, it looked sane,
I merged it, then thought it might be worth a couple of notes to the
list on this.
https://github.com/Exim/exim/pull/13
For those not already familiar: the "Files changed" tab is informative.
My general philosophy has been "we'll take contributions via any sane
means; we don't have so many contributors that we want to make people
jump through hoops, but we do _prefer_ to have things in our Bugzilla
for tracking. For non-contentious changes, working from a GitHub PR is
fine." (and I think I'm previously on record as saying that).
In your Exim repo, use `git config -e` (or `--edit`) to edit the
repository's config file (_usually_ found at `.git/config` relative to
the top level of the repo).
Add these lines:
----------------------------8< cut here >8------------------------------
[remote "github"]
fetch = +refs/heads/*:refs/remotes/github/*
fetch = +refs/pull/*/head:refs/remotes/github/pr/*
url = git@???:Exim/exim.git
----------------------------8< cut here >8------------------------------
Those assume that you're using SSH to talk to your GitHub account. Note
that there are _two_ `fetch` specifications, and the second one is
slightly unusual.
Git works mostly fine with multiple refspecs for a remote repo;
sometimes (or perhaps in some older versions of git) a `git fetch -p` to
prune will remove all the refs from the second entry, but a subsequent
fetch will restore them, no harm done. I tried just now, and that prune
misbehaviour no longer occurs.
With that fetch line, any pull request on GitHub becomes a remote branch
which you can work with locally in git. So I just did:
git checkout master
git pull # picked up Jeremy's latest changes
git fetch github
git merge --no-ff github/pr/13
git push
You can also do that sort of thing in the GitHub UI, but because GitHub
is not our canonical repository and gets content pushed to it from
git.exim.org, I strongly recommend against doing so. Instead, merge the
GitHub changes locally, then push to git.exim.org, and if you lose a
race and need to rebase or merge because someone else pushed in the
meantime, you can then resolve it there and then.
-Phil
