git-push
にリモート・リポジトリからブランチの削除を行うためのオプション、--delete
があることを知った。1.7.0で入ってたらしい。コロンつける奴は直ぐに忘れてしまうので、このオプションで覚える。SYNOPSISに載ってない……。
Release Noteによるとシンタックス・シュガーだということなので、
$ git push --delete origin foobar
が、
$ git push origin :foobar
と完全に等価ということみたい。はー覚えやすい。