Johannes Schindelin wrote:
Wrong. It cries out loud when you detach, not when you commit to a
detached HEAD. For good reason: Already at the second commit it would
stop being funny.
Right, I was wrong in expecting complaints. But... if it cried out at
the first commit, for many people there would probably not be a second.
Btw, I am ignorant on this: is there some case where one wants and has
reasons to commit to a detached head before making a temporary branch on it?
Furthermore, one could do just a bit more than detaching, namely store
the fact that head got detached and the name of the branch where the
head was. With this, when the unconscious user types git status or git
commit the system could alert him that head got detached because someone
updated the branch behind his shoulders from remote...
And of course, you need a way to show the user all the updates the branch
went through while the HEAD was detached, so that the user has a chance of
understanding what happened in the meantime.
So much additional work, just to fix up the shortcomings of the 'detach'
paradigm? I take it as a clear mark of a not-so-elegant design.
Well not that much additional work...
when you push to the checked out branch, head gets detached and branch
name (say /ref/heads/master) gets stored (say in .git/pre_push_branch).
when you run status or commit, you realize that there is a
pre_push_branch and you give the warning, saying what the
pre_push_branch was.
Now, since before the push you were at the tip of that branch, to know
what happened it should be enough to ask the log (or the diff) from
pre_push_branch to HEAD.
At the first user command that moves HEAD, pre_push_branch should get
deleted.
Btw, what does happen now if you delete the branch the remote worktree
is on? Don't you get a "dangling" head pointing to a non-existing branch
and the system claiming that it is at the initial commit? Maybe, this
too is a bit inelegant. In the other scenario, you would get a detached
head and in pre_push_branch the info the name of a no more existing
branch (mainig clear that you were on a branch that got deleted) and
this info could be returned to the user.
Of course, I am not claiming that forbidding pushes to branches with
checked out tree is bad. It is a good idea in my opinion.
I am just suggesting that one still wanting to allow that push in spite
of all the potential consequences (namely wanting to mess with the
relevant config variable), might prefer detaching head, storing the
pre_push_branch and getting some info on status and commit rather than
merely allowing the push.
In fact, I believe that the point is that with the current push-allowing
behavior, when the push happens you loose the information about the
precise commit against which the changes in the worktree were made.
Which might be a useful piece of info.
Ciao,
Sergio
--
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
