From: Marius Paliga Date: Mon, 23 Oct 2017 11:44:49 GMT Subject: [PATCH] builtin/push.c: add push.pushOption config Message-ID: <20171023114449.11902-1-marius.paliga@gmail.com> In-Reply-To: Push options need to be given explicitly, via the command line as "git push --push-option