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