[PATCH v3 3/9] user-manual: Give 'git push -f' as an alternative to +master
From: "W. Trevor King" <wking@tremily.us>
This mirrors existing language in the description of 'git fetch'.
Signed-off-by: W. Trevor King <wking@tremily.us>
---
Documentation/user-manual.txt | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
index dbffd0a..ba06b7e 100644
--- a/Documentation/user-manual.txt
+++ b/Documentation/user-manual.txt
@@ -2051,6 +2051,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.
--
1.8.1.336.g94702dd
W. Trevor King <wking@tremily.us>