TIL: Checking out a PR from a different repo locally
Somebody’s submitted a pull request on GitHub to your project. They didn’t have write access to your repo, so they forked it, then did their changes (either in the main or another branch).
You want to check those changes out locally, maybe make a few edits, then merge to main on your repo. GitHub’s inline commands help if you want to merge the PR’s branch locally, but I always trip up on how to handle the “muck about and make some changes” scenario. Here’s how (replace {placeholders} with proper values):
# add the other repository as a remote (the URL to add should be at the bottom of the PR)
git remote add {contributing_username} git@github.com:{contributing_username}/{repository}.git
# get git a sitrep of the other repo
git fetch {contributing_username}
# create a new local branch, based on the branch from the PR
git checkout -b {contributing_username}-{branch} {contributing_username}/{branch}
Now you have a local branch that mirrors whatever’s in the contributing repository’s branch. Want to make some changes?
If the contributor has enabled “Allow edits from maintainers” in their PR, you can git push and update the PR branch directly (in the other person’s repo!). Then you can handle merging and closing the PR through GitHub’s UI. Here’s how to push to the right place:
# make sure the other repo’s branch is set as upstream for your branch
git branch {contributing_username}-{branch} -u {contributing_username}/{branch}
# push commits in your current branch to {branch} from the PR
git push {contributing_username} HEAD:{branch}
Otherwise, you can make and commit any edits, merge to your main branch (ideally with a merge commit indicating you’re closing the PR #, use git merge --no-ff to ensure there’s a merge commit), then push, updating your repo and automatically closing the PR in the process.
With thanks to: