# HG changeset patch
# User Oleksandr Gavenko <gavenkoa@gmail.com>
# Date 1520083522 -7200
# Node ID d0c386e6f03985bc3e4aca10dfe974facd306e24
# Parent  ac7f6d8bea28ed30b4afc9f1f1e1b73da47a38bc
Undo mistaken push.

diff -r ac7f6d8bea28 -r d0c386e6f039 git.rst
--- a/git.rst	Sat Mar 03 15:22:58 2018 +0200
+++ b/git.rst	Sat Mar 03 15:25:22 2018 +0200
@@ -417,6 +417,12 @@
   $ git reset --hard $HASH
   $ git push -u origin master --force
 
+You can delete remote branch with syntax of appended colon before branch name::
+
+  $ git reset HEAD^
+  $ git push origin :$NAME
+  $ git push origin $NAME
+
 Git bisect
 ==========