git tips: git push $remote HEAD で現在のブランチを$remoteにpushできて、コマンドラインでgitを使うときはよく使います。 ところで、この HEAD の実体はファイル（.git/HEAD）なので、ファイルシステムが大文字小文字を無視する（case-insensitive; e.g. …