My question is related to the discussion in Contributing to an existing pull request.

Gajus explained that GitHub made it possible for repo owners to edit a a contributor's PR by pushing commits directly to the PR branch on their fork.

That's good. But as part of his explanation, there was this command in the terminal:

git push contributor-origin HEAD:branch-name

Why do we have to add the HEAD: prefix in front of the branch name for this to work? I tried pushing directly to branch-name but I got this error:

error: failed to push some refs to REPO
hint: Updates were rejected because a pushed branch tip is behind its remote
hint: counterpart. Check out this branch and integrate the remote changes
hint: (e.g. 'git pull ...') before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.

CodePudding user response：

git push upstream x:y simply says "on upstream, push my commit x to branch y".

git push upstream branch-name is a shortcut for git push upstream branch-name:branch-name.

You will get the error message you mention if the commit x you push is not a fast forward of y.

In the situation you describe, it so happened that :

• at the time you ran git push upstream HEAD:branch, your active commit was ahead of branch,
• at the time you ran git push upstream branch, your local branch wasn't ahead of it's remote counterpart.

Run git fetch upstream and inspect how upstream/branch evolved.