[exim-dev] Working with GitHub PRs

Αρχική Σελίδα
Delete this message
Reply to this message
Συντάκτης: Phil Pennock
Ημερομηνία:  
Προς: exim-dev
Αντικείμενο: [exim-dev] Working with GitHub PRs
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