we have --delete now

Author: schacon

book/03-git-branching/1-git-branching.asc

@@ -775,22 +775,17 @@ There are other uses of the `pull` command that we'll address in [[_git_tools]],
 ==== Deleting Remote Branches
 
 Suppose you're done with a remote branch – say you and your collaborators are finished with a feature and have merged it into your remote's `master` branch (or whatever branch your stable codeline is in).
-You can delete a remote branch using the rather obtuse syntax `git push [remotename] :[branch]`.
+You can delete a remote branch using the `--delete` option to `git push`.
 If you want to delete your `serverfix` branch from the server, you run the following:
 
 [source,shell]
 ----
-$ git push origin :serverfix
-To git@github.com:schacon/simplegit.git
+$ git push origin --delete serverfix
+To https://github.com/schacon/simplegit
  - [deleted]         serverfix
 ----
 
-Boom.
-No more branch on your server.
-You may want to dog-ear this page, because you'll need that command, and you'll likely forget the syntax.
-
-A way to remember this command is by recalling the `git push [remotename] [localbranch]:[remotebranch]` syntax that we went over a bit earlier.
-If you leave off the `[localbranch]` portion, then you're basically saying, ``Take nothing on my side and make it be `[remotebranch]`.''
+Basically all this does is remove the pointer from the server. The Git server will generally keep the data there for a while until a garbage collection runs, so if it was accidentally deleted, it's often easy to recover.
 
 === Rebasing