[PATCH] Docs: Describe omitted <repository> behavior in a prominent place

[Ori Avtalion <ori@avtalion.name>]

The documentation of which repository is pushed to when the repository
flag is omitted was only mentioned under the --repo flag.

It is now described under the <repository> argument.

Signed-off-by: Ori Avtalion <ori@avtalion.name>
---
 Documentation/git-push.txt |   15 +++++++++------
 1 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index 59dc8b1..14d286e 100644
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -31,6 +31,11 @@ OPTIONS[[OPTIONS]]
 	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).
++
+If omitted, 'git push' derives the remote name from the current
+branch: If it tracks a remote branch, then that remote repository
+is pushed to. Otherwise, the name "origin" is used. This can be
+overridden with the `--repo` option.
 
 <refspec>...::
 	The format of a <refspec> parameter is an optional plus
@@ -116,12 +121,10 @@ nor in any Push line of the corresponding remotes file---see below).
 
 --repo=<repository>::
 	This option is only relevant if no <repository> argument is
-	passed in the invocation. In this case, 'git push' derives the
-	remote name from the current branch: If it tracks a remote
-	branch, then that remote repository is pushed to. Otherwise,
-	the name "origin" is used. For this latter case, this option
-	can be used to override the name "origin". In other words,
-	the difference between these two commands
+	passed in the invocation, and the current branch does not track
+	a remote branch. For this case, this option can be used to 
+	override the name "origin". In other words, the difference
+	between these two commands
 +
 --------------------------
 git push public         #1
-- 
1.7.0