Andy Parkins [off-list ref] writes:
Why does a bare repository have/need a HEAD?
To mark which branch the repository owner considers the primary
branch of the repository. I think "git pull $URL" (i.e. without
using shorthand arranged in the config nor $GIT_DIR/remotes/)
defaults to fetching and merging HEAD from there, for example (I
say "I think" because it's been a while I did so myself, and we
might have broken it during the 1.5.0 process, which had a lot
of work in that area).