Getting notified that my first pull request got merged was exciting. The process was a great learning experience. After the merge I wanted to clean up my branch. Github provides a nice GUI interface for deleting branches. After a pull request is merged a delete button appears in the pull request page along with a message indicating it is now safe to delete. But I also had other test branches that weren’t merged that needed to be deleted too.
This deletes branch
issue2235-bad from our local machine. The colon tells git we want to delete. I used capital -D to force it to delete since I know I no longer need it.
git branch -D :issue2235-bad
This deletes the branch from our remote
git push origin :issue2235-bad