On Thursday, January 20, 2011 10:32:40 Felipe Contreras wrote: > Hi, > > On Thu, Jan 20, 2011 at 1:14 PM, Stephen Kelly <steveire@xxxxxxxxx> wrote: > > Stephen Kelly wrote: > >> On Friday we had an issue where a developer pushed a branch called > >> HEAD to the remote server. The result was that other developers could > >> not pull or push. [...] > Which version of git? > Which kind of network transport was used? > Is this reproducible? FWIW, here is a quick demonstration of at least one problem with having a branch called HEAD. You can make it and push it fine, but when cloning, you don't get it. #!/bin/bash git init --bare origin.git git clone origin.git wc1 cd wc1 git commit --allow-empty -m "Initial rev" git checkout -b HEAD git commit --allow-empty -m "Make HEAD branch" git push --all cd .. git clone origin.git wc2 diff -u <(cd wc1; git branch -a) <(cd wc2; git branch -a) diff -u <(cd wc1; git log --all) <(cd wc2; git log --all) If I do the following from wc2 I can get the branch manually: git pull origin refs/heads/HEAD:HEAD I haven't played with it enough to see what other problems might arise. -- 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