Is it by design you can create a branch called 'HEAD'?

One of our devs managed to push a branch called HEAD into our master repository, which then caused various failures for people doing pulls.

   c2014aa..cbe0021  trunk      -> origin/trunk
error: Ref refs/remotes/origin/trunk is at
cbe002152fcc917216ad9003037309893f09901d but expected
c2014aa485130013ca7eda1cb4a4eef192f9406d
 ! c2014aa...2bb416b HEAD       -> origin/HEAD  (unable to update local ref)

And warnings like:

$ git log HEAD warning: refname 'HEAD' is ambiguous.

(we renamed master to 'trunk' long ago for various reasons)

In order to clean it up we found that there was an entry

2bb416bb4a44fbd61f29479d63a95705a7044e32 refs/heads/HEAD

in our master packed-refs file, along with the normal HEAD file:

$ cat HEAD ref: refs/heads/trunk $ cat refs/heads/trunk 0752c05e75dd645833fb0ea7ce8e534cbd603f0b

I deleted that line and then we removed these (output of find -ls)

20119672 0 -rw-rw-r-- 1 root cvs 0 May 21 01:26 ./logs/refs/remotes/origin/HEAD 20120092 4 -rw-rw-r-- 1 root cvs 162 May 21 01:26 ./logs/refs/heads/HEAD

And things seemed to be fine. (yes we hillariously call our git user group cvs :-)

So I am wondering, did we do the cleanup right? Is this behavior by design? What is the most appropriate way to prevent it from happening again?

I will try to find out from the responsible dev if they have their command history available to see what they did.

cheers, Yves