Re: Minor annoyance with git push

[Junio C Hamano <gitster@pobox.com>]

Jeff King <peff@peff.net> writes:

> Thinking about this more, this situation is more than a minor annoyance:
> it is actually somewhat dangerous. If you ever wanted to push _one_
> non-ff case (say, for your current branch) and you were to use "git push
> -f", you would rewind history for random branches, and sorting the mess
> out at the remote could be awful (especially if it is a bare repo
> without reflogs).

Yeah, -f using "matching refs" is dangerous, but on the other
hand, that would be how you correct that mistake in one shot,
after you fixed the mistake locally.

Is there anything wrong with "git push $there $branch_name"?  I
thought we discussed this last time and there was even a patch
that does "git push $there HEAD" to push out the current branch,
which I am fairly sure that I accepted (but I do not remember,
as I do not use such a shorthand. When I want to push a single
branch, I _want_ to be explicit, to make sure I push out the
right thing).

So after doing a fix on a single branch, you would:

	$ git push origin HEAD

and you are done.  No need to spell out the long branch name you
are currently on.

I do not know if this was part of the last round of patches, but
I suspect it is not a problem to allow

	$ git push HEAD

if it is unambiguous.  That is, "HEAD?  Do we have such a remote
nickname?  No.  Then can we default to 'origin' and use it as
the ref to push?  Yeah, we can, so the user meant 'git push
origin HEAD'".