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

Marius Paliga [off-list ref] writes:

Push options need to be given explicitly, via the command line as "git
push --push-option <option>".  Add the config option push.pushOption,
which is a multi-valued option, containing push options that are sent
by default.

When push options are set in the lower-priority configulation file
(e.g. /etc/gitconfig, or $HOME/.gitconfig), they can be unset later in
the more specific repository config by the empty string.

Add tests and update documentation as well.

Signed-off-by: Marius Paliga <redacted>
---

Looks good.

+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

s/cofig/config/; I think you inherited from me, sorry.

I'll tweak it while queuing; there is not need to resend only to fix
this.

Thanks.