git tips: git push $remote HEAD
で現在のブランチを$remoteにpushできて、コマンドラインでgitを使うときはよく使います。
ところで、この HEAD
の実体はファイル(.git/HEAD
)なので、ファイルシステムが大文字小文字を無視する(case-insensitive; e.g. macOSのデフォルト)ときは、 git push $remote head
でも動いてしまいます。しかしこれを習慣にしていると、大文字小文字を無視しないファイルシステムで動かずハマることがあります(というかまあ、ハマってしばらく悩みました)。普段から HEAD
とタイプする習慣にしておくとよいと思います。