Fix checking out a different branch while pushing a branch for the first time #4214
+11
−4
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When pushing a branch that didn't have an upstream yet, we use the command line
git push --set-upstream origin HEAD:branch-name
The HEAD: part of this is too unspecific; when checking out a different branch while the push is still running, then git will set the upstream branch on the newly checked out branch, not the branch that was being pushed. This might be considered a bug in git; you might expect that it resolves HEAD at the beginning of the operation, and uses the result at the end.
But we can easily work around this by explicitly supplying the real branch name instead of HEAD.
Fixes #4207.
go generate ./...
)