Re: Pushing into a repository with working directory?

From: Shawn O. Pearce <spearce@spearce.org>
Date: Jan 9, 2007, 03:32 UTC
Message-ID: <20070109033213.GC1904@spearce.org>
In-Reply-To: <7vd55pt3ts.fsf@assigned-by-dhcp.cox.net>

Junio C Hamano <junkio@cox.net> wrote:

Show 9 quoted lines

> However, I am not sure if that is easy to understand for the
> users.  It would be sane to deny pushing into the current branch
> for a non-bare repositories by default, and if we do allow it
> (perhaps with 'git-push --force'), then detach the HEAD as you
> suggest.  On the other hand, pushing into the current branch of
> a bare repository should just work; the HEAD pointer in a bare
> repository is not about the commit the index and the working
> tree are based on, but which branch is the primary branch of the
> repository.

But from the working directory management tools' perspective HEAD *is* about the current index and the current working directory. If HEAD doesn't match the index and working directory closely enough then the user is going to do something stupid, like commit a negative delta by accident.

Pushing into the current branch of a repository with a working directory probably shouldn't be allowed by default as users probably don't want to do that. But if --force is used then detaching the HEAD is probably the best idea. The user could easily recover by doing `git checkout origbranch` (though they may need `git checkout -m origbranch` if their working directory was dirty).

-- 
Shawn.