user-manual: give 'git push -f' as an alternative to +master

This mirrors existing language in the description of 'git fetch'.

Signed-off-by: W. Trevor King <wking@tremily.us>
Signed-off-by: Junio C Hamano <gitster@pobox.com>

diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
index 74dd82ab7ad7215f589f92376c9549082975d3a7..a546b10ee1c6a12bc9e856f137f65db6e4bf1ba0 100644 (file)
--- a/Documentation/user-manual.txt
+++ b/Documentation/user-manual.txt
@@ -2045,6 +2045,13 @@ branch name with a plus sign:
 $ git push ssh://yourserver.com/~you/proj.git +master
 -------------------------------------------------
 
 $ git push ssh://yourserver.com/~you/proj.git +master
 -------------------------------------------------
 

+Note the addition of the `+` sign.  Alternatively, you can use the
+`-f` flag to force the remote update, as in:
+
+-------------------------------------------------
+$ git push -f ssh://yourserver.com/~you/proj.git master
+-------------------------------------------------
+

 Normally whenever a branch head in a public repository is modified, it
 is modified to point to a descendant of the commit that it pointed to
 before.  By forcing a push in this situation, you break that convention.
 Normally whenever a branch head in a public repository is modified, it
 is modified to point to a descendant of the commit that it pointed to
 before.  By forcing a push in this situation, you break that convention.