-
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>
d8052750