Documentation: git push repository can also be a remote

This is copied from pull-fetch-param.txt and helps the reader
to not get stuck in the URL section.

Signed-off-by: Anders Melchiorsen <redacted>
Signed-off-by: Junio C Hamano <redacted>

diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index 3321966c6b802e575fcd3f67969ccc4e8572925e..8bfa7cb7e5dbd878ad244db4fabf1e899cb61a2a 100644 (file)
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -28,7 +28,9 @@ OPTIONS
 -------
 <repository>::
        The "remote" repository that is destination of a push
-       operation.  See the section <<URLS,GIT URLS>> below.
+       operation.  This parameter can be either a URL
+       (see the section <<URLS,GIT URLS>> below) or the name
+       of a remote (see the section <<REMOTES,REMOTES>> below).
 
 <refspec>...::
        The canonical format of a <refspec> parameter is