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 = [email protected]: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

Attachment: pgpQzlRI5T4rh.pgp
Description: PGP signature

-- 
## List details at https://lists.exim.org/mailman/listinfo/exim-dev Exim 
details at http://www.exim.org/ ##

Reply via email to