From: Chris Rorvick <chris@rorvick.com>
Date: Fri, 26 Oct 2012 13:59:58 GMT
Subject: Re: git push tags
Message-ID: <CAEUsAPZC80aSwnS0sBTt9nEu0HgyPp0BD2TWjSBb7tS7=i=VhQ@mail.gmail.com>
In-Reply-To: <CAM9Z-n=+YeF3BaF-5UB5f2GBHYw7WDZEFDVT72RGSsDBaH4PJA@mail.gmail.com>

On Fri, Oct 26, 2012 at 8:37 AM, Drew Northup <n1xim.email@gmail.com> wrote:
> (As for deleting the current branch, you can't really do that on a
> proper bare remote anyway as there is no such thing as a "current
> branch" in that context.)

Really?  When I clone a bare repository I see a HEAD, and Git doesn't
want me to delete it with a push from a remote repo.  So is this not a
"proper" bare repository?