Undo mistaken push.
authorOleksandr Gavenko <gavenkoa@gmail.com>
Sat, 03 Mar 2018 15:25:22 +0200
changeset 2233 d0c386e6f039
parent 2232 ac7f6d8bea28
child 2234 30fb3f7626e3
Undo mistaken push.
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
 ==========