There is a "git remote set-head" to manipulate HEAD in a remote
repository.
Thanks, that is useful (like git symbolic-ref HEAD master-x suggested by
Kevin, much better than editing the text file)
I agree that this might be viewed as a user experience issue.
But I can not come up with a possible solution. Can you?
The branch where the user was when he/she pushed the repo to the server?
it would be his/her responsibility to checkout the proper branch before
pushing... if that was not good enough than he/she could always use git
remote set-head... my point is: pointing to a bad branch that exists
seems better than pointing to a branch that does not exist...
Anyway I agree this is not important, as we can easily change HEAD.
I do not think there should be any issues.
Thank you very much for your answers,
Carlos
--
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