From: Junio C Hamano <gitster@pobox.com>
Date: Tue, 30 Oct 2007 08:28:43 GMT
Subject: Re: [PATCH 04/10] push: add "git push HEAD" shorthand for 'push current branch to default repo'
Message-ID: <7v8x5lngzo.fsf@gitster.siamese.dyndns.org>
In-Reply-To: <11935935812185-git-send-email-prohaska@zib.de>

Will drop this as you already know why.