But practically speaking... is there that many cases where a branch is
updated directly instead of the operation performed through HEAD?
We identified one case which is a push to a non bare repo.
If those cases are very few (and they _should_ be very few) then we
might simply cheat a little and update HEAD separately in those cases.
Nicolas
-
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at http://vger.kernel.org/majordomo-info.html