diff options
Diffstat (limited to 'src/util/git-push-everything.pl')
| -rwxr-xr-x | src/util/git-push-everything.pl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util/git-push-everything.pl b/src/util/git-push-everything.pl index faebdf7..ee39ab4 100755 --- a/src/util/git-push-everything.pl +++ b/src/util/git-push-everything.pl @@ -33,6 +33,12 @@ die unless -e "$git_master_repo/.git"; print "Formaline: Pushing source tree to master git repository...\n"; +print "Executing: $git_cmd config receive.denyCurrentBranch false\n" unless $silent; +system "$git_cmd --git-dir=$git_master_repo/.git config receive.denyCurrentBranch false $silencer"; +if ($?) { + die "Formaline: WARNING: Error while configuring master git repository"; +} + print "Executing: $git_cmd push -v -f --all $git_master_repo\n" unless $silent; system "$git_cmd push -v -f --all $git_master_repo $silencer"; if ($?) { |