GitHub has the cool feature where while opening a pull request one can allow the maintainers to push changes to that branch. This is a lot more ergonomic than suggesting larger-scale edits in the insufferably slow GitHub web UI. But it does require setting up remotes and upstream branches correctly.
Smarter people than me wrote scripts to do this for them, but I’ve landed on using the official GitHub CLI tool and its gh repo co PR-NUMBER feature, which leads to the first key point: the gh tool is great to interact with GitHub.
If you check out a pull request that way, it sets everything up so you can git push and git pull as if it were your own branch.
All push, no pull
Only… it didn’t work for me! I could push alright, but when I merged main into someone else’s pull request branch in the web UI and ran git pull --rebase on my computer, I got:
Your configuration specifies to merge with the ref 'refs/heads/pr-branch'
from the remote, but no such ref was fetched.
After complaining about it on all social medias, Tomáš Janoušek helped me troubleshoot this and found the problem immediately:
I’ve had fetch.all=true set in my .gitconfig1 and after removing that, git pull started working as advertised.
And now I’m off to learn Jujutsu VCS…
Please don’t ask me why I’ve set anything in my
.gitconfig. It’s a 20-year masterpiece of random copy-pasting. ↩︎
