From d8052750c5fdd53cb5a664a18ce9d78dbedb22ae Mon Sep 17 00:00:00 2001 From: Marius Paliga Date: Mon, 23 Oct 2017 13:44:49 +0200 Subject: [PATCH] builtin/push.c: add push.pushOption config Push options need to be given explicitly, via the command line as "git push --push-option