Re: [PATCH] builtin/push.c: add push.pushOption config

[Junio C Hamano <gitster@pobox.com>]

Junio C Hamano <gitster@pobox.com> writes:

>> We'd also want to document how push.pushOption works in
>> Documentation/config.txt (that contains all the configs)
>
> Perhaps.

Here is my attempt.  I have a feeling that the way http.extraheaders
is described may be much easier to read and we may want to mimick
its style.  I dunno.

 Documentation/config.txt | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Documentation/config.txt b/Documentation/config.txt
index 1ac0ae6adb..631ed1172e 100644
--- a/Documentation/config.txt
+++ b/Documentation/config.txt
@@ -2621,6 +2621,16 @@ push.gpgSign::
 	override a value from a lower-priority config file. An explicit
 	command-line flag always overrides this config option.
 
+push.pushOption::
+	When no `--push-option=<option>` argument is given from the
+	command line, `git push` behaves as if each <value> of
+	this variable is given as `--push-option=<value>`.
++
+This is a multi-valued variable, and an empty value can be used in a
+higher priority cofiguration file (e.g. `.git/config` in a
+repository) to clear the values inherited from a lower priority
+configuration files (e.g. `$HOME/.gitconfig`).
+
 push.recurseSubmodules::
 	Make sure all submodule commits used by the revisions to be pushed
 	are available on a remote-tracking branch. If the value is 'check'