Re: push.default documented in "man git-push"?

[Ramkumar Ramachandra <artagnon@gmail.com>]

David Glasser wrote:
> Is the newish push.default documented in the "git push" manpage
> anywhere? I don't see it mentioned (and there are several references
> to the "default" behavior), but maybe I'm missing something. Is it
> left out on purpose (ie, config values aren't supposed to be mentioned
> in command manpages)?

You're right.  It's documented in `man git-config`, but we should
probably mention it in the `git-push` manpage.

--8<--
From: Ramkumar Ramachandra <artagnon@gmail.com>
Date: Tue, 2 Oct 2012 20:37:13 +0530
Subject: [PATCH] Documentation: mention `push.default` in git-push.txt

Signed-off-by: Ramkumar Ramachandra <artagnon@gmail.com>
---
 Documentation/git-push.txt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index cb97cc1..8751b38 100644
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -37,7 +37,8 @@ OPTIONS[[OPTIONS]]
        `+`, followed by the source ref <src>, followed
        by a colon `:`, followed by the destination ref <dst>.
        It is used to specify with what <src> object the <dst> ref
-       in the remote repository is to be updated.
+       in the remote repository is to be updated.  If not specified,
+       the configuration variable `push.default` is used.
 +
 The <src> is often the name of the branch you would want to push, but
 it can be any arbitrary "SHA-1 expression", such as `master~4` or
-- 
1.7.12.1.428.g652398a.dirty