These commands can be used to remote a branch both from the local repository and from the remote repository.
$ git push origin --delete <branch_name> $ git branch -d <branch_name>
-d will probably have to be replaced by
-D if the branch has not been merged.
Was this useful to you? Yes NoTags: