One Quickie

---

Deleting a remote git branch (git->Hacks)

Say you had a branch name "protocol-play" that's been pushed up to github. To remove it locally you do the usual git branch -D protocol-play (the capital D if you don't care about the merged status). You might need to git push. too.

It's gone locally, but still exists up on github. Nuke it there with:

% git push origin :protocol-play