user-manual: reset to ORIG_HEAD not HEAD to undo merge

diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
index 7b6dc22e7bad8bfc3d6f018e47e2025f2a1508ee..e37a1234fa27752b01c53536299079b6d669e941 100644 (file)
--- a/Documentation/user-manual.txt
+++ b/Documentation/user-manual.txt
@@ -1255,7 +1255,7 @@ $ git reset --hard HEAD
 Or, if you've already commited the merge that you want to throw away,
 
 -------------------------------------------------
-$ git reset --hard HEAD^
+$ git reset --hard ORIG_HEAD
 -------------------------------------------------
 
 However, this last command can be dangerous in some cases--never