Working on a PR on django/djangoproject.com, a question came up about how to rebase if the GitHub UI doesn't offer exactly what you want:
What do you usually do in these situations?
So, since you have write access, and assuming "Allow edits by maintainers" is checked (which is almost always, being the default) you can push to the contributor branch.
The PR was number 963. So to checkout the PR locally you can do:
git fetch origin pull/963/head:pr/963
This pulls the branch from this PR to a local branch pr/963
.
You can then check that out.
I have it as an alias:
% cat ~/.gitconfig| grep 'pr ='
pr = !sh -c \"git fetch origin pull/${1}/head:pr/${1} && git checkout pr/${1}\"
So I do git pr 936
to fetch and checkout the branch.
I then rebase... so git pull --rebase origin main
— but I usually use the awesome Fork GUI
Then to push you look at the top where it says ... into django:main from pauloxnet:feature/update_docs_and_index
— you can use the icon to copy the pauloxnet:feature/update_docs_and_index
which is the username:branchname
pair.
Then to push it's:
git push -f git@github.com:pauloxnet/djangoproject.com HEAD:feature/update_docs_and_index
-f
https://github.com
.pauloxnet/djangoproject.com
is the remote — you get the username from the username:branchname
pair you copied beforeHEAD
is your checkedout out version of the PR — what you're pushing. feature/update_docs_and_index
is the other part of the username:branchname
pair you copied before.I use a TextExpander snippet to map from one to the other, but any of a million similar tools are worthwhile.
The other git alias I use all the time is to reset a local branch to a PR, if the user pushed updates:
~ % cat ~/.gitconfig| grep 'pr-reset'
pr-reset = !sh -c \"git fetch origin pull/${1}/head && git reset --hard FETCH_HEAD\"
This is the same fetch
as before, but instead of creating the local branch it hard resets to the remote state. I do git pr-reset 963
to reset to the latest remote state.