summaryrefslogtreecommitdiff
path: root/Documentation/user-manual.txt
diff options
context:
space:
mode:
authorW. Trevor King <wking@tremily.us>2013-02-17 19:15:55 -0500
committerJunio C Hamano <gitster@pobox.com>2013-02-18 00:48:37 -0800
commitd1471e061657c2e437076947e0e51a3c32adfa60 (patch)
treea63b94bdeebd2f2fcd2ee3bd251791bfa7264e37 /Documentation/user-manual.txt
parente9b4908302c659251a47ce440676cb3b0d65b8af (diff)
downloadgit-d1471e061657c2e437076947e0e51a3c32adfa60.tar.gz
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>
Diffstat (limited to 'Documentation/user-manual.txt')
-rw-r--r--Documentation/user-manual.txt7
1 files changed, 7 insertions, 0 deletions
diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
index 74dd82ab7a..a546b10ee1 100644
--- 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
-------------------------------------------------
+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.