git push --del⁠e⁠t⁠e

git-pushにリモート・リポジトリからブランチの削除を行うためのオプション、--deleteがあることを知った。1.7.0で入ってたらしい。コロンつける奴は直ぐに忘れてしまうので、このオプションで覚える。SYNOPSISに載ってない……。

Release Noteによるとシンタックス・シュガーだということなので、

$ git push --delete origin foobar

が、

$ git push origin :foobar

と完全に等価ということみたい。はー覚えやすい。