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>
W. Trevor King committed
Feb 17, 2013 at 19:15 UTC
d1471e061657c2e437076947e0e51a3c32adfa60
1 file changed
+7
Documentation/user-manual.txt
+7
@@ -2045,6 +2045,13 @@ branch name with a plus sign:
2045
$ git push ssh://yourserver.com/~you/proj.git +master
2046
-------------------------------------------------
2047
2048
+Note the addition of the `+` sign. Alternatively, you can use the
2049
+`-f` flag to force the remote update, as in:
2050
+
2051
+-------------------------------------------------
2052
+$ git push -f ssh://yourserver.com/~you/proj.git master
2053
+-------------------------------------------------
2054
+
2055
Normally whenever a branch head in a public repository is modified, it
2056
is modified to point to a descendant of the commit that it pointed to
2057
before. By forcing a push in this situation, you break that convention.