builtin/push.c: add push.pushOption config
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 <marius.paliga@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>