Each GitHub pull request is associated with a reference in the target repository. For instance the commit sent to pull request 3948 is the reference refs/pull/3948/head. If GitHub successfully merges the pull request in the target branch, another reference is associated with it, for instance refs/pull/3948/merge.
It is convenient to mirror pull requests in local branches, for instance to trigger GitLab CI or jenkins git-plugin because they only react to commits that belong to branches, not orphaned references. The tip of the branch can be named pull/XXX and its tip reset to the matching merge reference.
The tip of the branch could be set to the head reference but it would be less effective than using the merge because it is based on an older version of the target branch. Whatever test runs on the head, it may fail although it could succeed after the merge.
GitHub does not set the merge and the head reference atomically: the head can be set before GitHub even tries to merge. Similarly, when a pull request is rebased and forced push, there is a window of opportunity for the merge reference to still be about the previous head.
The following shell function takes care of all these border cases and keeps an up to date set of branches accurately reflecting all pull requests from a GitHub repository:
function import_pull_requests() {
local remote=$1
local ref
local remote_head
git fetch $remote +refs/pull/*:refs/remotes/$remote/pull/*
git for-each-ref \
--sort='-committerdate' \
--format='%(refname) %(objectname)' \
refs/remotes/$remote/pull/*/head | \
while read ref remote_head ; do
local pr=$(echo $ref | perl -pe 's:.*/pull/(.*)/head:$1:')
# ignore pull requests that cannot merge
local merge=$(git rev-parse --quiet --verify
refs/remotes/$remote/pull/$pr/merge)
test -z "$merge" && continue
# ignore pull requests for which the merge does not match the
# remote head, most likely because it has not been updated yet
# after a rebase was pushed
local merged_head=$(git rev-parse
refs/remotes/$remote/pull/$pr/merge^2)
test "$merged_head" != "$remote_head" && continue
# nothing to do if the head did not change since we last saw
# it
local local_head=$(git rev-parse --quiet --verify
refs/pull/$pr/head)
test "$remote_head" = "$local_head" && continue
# remember the head for the next round
git update-ref refs/pull/$pr/head $remote_head
# create/update a branch with the successfull merge of the
# head
git update-ref refs/heads/pull/$pr $merge
echo branch pull/$pr
done
}