diff options
| author |  W. Trevor King <wking@tremily.us> | 2013-02-17 19:15:55 -0500 |
|---|---|---|
| committer |  Junio C Hamano <gitster@pobox.com> | 2013-02-18 00:48:37 -0800 |
| commit | d1471e061657c2e437076947e0e51a3c32adfa60 (patch) | |
| tree | a63b94bdeebd2f2fcd2ee3bd251791bfa7264e37 /Documentation/user-manual.txt | |
| parent | user-manual: use 'remote add' to setup push URLs (diff) | |
| download | tgif-d1471e061657c2e437076947e0e51a3c32adfa60.tar.xz | |
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.txt | 7 |
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. |