push: make push.default = current use resolved HEAD
commit0f075b220862e729eb3873a1c1496b923d17c2d4
authorRamkumar Ramachandra <artagnon@gmail.com>
Wed, 29 May 2013 19:21:51 +0000 (30 00:51 +0530)
committerJunio C Hamano <gitster@pobox.com>
Wed, 29 May 2013 22:34:07 +0000 (29 15:34 -0700)
tree90d4ab00ca754ec4108d57e5ddbfde21f1804088
parent7b2ecd81084adeba701c60da81eec6be478910b8
push: make push.default = current use resolved HEAD

With this change, the output of the push (with push.default set to
current) changes subtly from:

  $ git push
  ...
   * [new branch]      HEAD -> push-current-head

to:

  $ git push
  ...
   * [new branch]      push-current-head -> push-current-head

This patch was written with a different motivation. There is a problem
unique to push.default = current:

  # on branch push-current-head
  $ git push
  # on another terminal
  $ git checkout master
  # return to the first terminal
  # the push tried to push master!

This happens because the 'git checkout' on the second terminal races
with the 'git push' on the first terminal.  Although this patch does not
solve the core problem (there is still no guarantee that 'git push' on
the first terminal will resolve HEAD before 'git checkout' changes HEAD
on the second), it works in practice.

Signed-off-by: Ramkumar Ramachandra <artagnon@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
builtin/push.c