This is a placeholder for things I do in
git which I have to look up often.
Remove a branch from git
git push origin --delete branch_name git branch -d branch_name
If there are unmerged changes which you are confident of deleting:
git branch -D branch_name
References article how to remove git branches.