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>