Make sure the main git repo is case-insensitive too

1 files changed, 3 insertions, 0 deletions

diff --git a/sync-all b/sync-all
index a7b579ed99..06c183af25 100755
--- a/sync-all
+++ b/sync-all
@@ -283,6 +283,9 @@ sub scmall {
             if (-d $localpath) {
                 warning("$localpath already present; omitting")
                     if $localpath ne ".";
+                if ($scm eq "git") {
+                    scm ($localpath, $scm, "config", "core.ignorecase", "true");
+                }
                 next;
             }