push¶
Push local branch to a remote and make make remote use different branch name.
$ git push origin dev-feature:dev-foo-barremove remote branch¶
New approach since git >= 1.7:
$ git push origin --delete <branch-name>Then this on other machines to propagate the changes:
$ git fetch --all --pruneOr, for those used to the approach git push local_branch:remote_branch, then this might also be easy to remember, remove the remote branch with (note space before the :):
$ git push origin :remote_branch_to_deleteReferences:
- stack overflow post
git push --help