Re: Pushing into a repository with working directory?

["Shawn O. Pearce" <spearce@spearce.org>]

Junio C Hamano <junkio@cox.net> wrote:
> 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.