Re: git push to a non-bare repository

On Mon, 19 Mar 2007, Theodore Tso wrote:

On Mon, Mar 19, 2007 at 12:08:47AM -0400, Nicolas Pitre wrote:

quoted

If the meaning of HEAD changed (although indirectly) because HEAD 
happens to point to the branch that just got updated then logically the 
HEAD reflog should be updated too.  On the other hand the HEAD reflog 
should reflect operations performed on HEAD.  Since the push updates the 
branch directly it is not exactly performing some operation on HEAD 
since HEAD could point anywhere and that wouldn't change the push at 
all.

Meaning that for the discussion of pushing to a non-bare repository with 
a dirty working tree... If the branch being pushed into is not pointed 
to by HEAD then no consideration what so ever about the working tree 
should be made, and no update to the HEAD reflog made of course.

Right, but if the branch being pointed to is pointed to by HEAD I
would argue that the reflog for HEAD should be updated, since
operations that reference HEAD will see a new commit, and and it will
be confusing when "git reflog" shows no hint of the change.

Of couse, if the branch being pushed to isn't one which is pointed by
HEAD, of course HEAD's reflog shouldn't be updated.

I think we're saying the exact same thing.


Nicolas