Avoid --no-tags option

We don't use tags anyway, so it's not making a difference, and is only supported by relatively new git.
ncough · Nov 28, 2017 · 11694c3 · 11694c3
1 parent a503ecb
commit 11694c3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/worker.sml b/worker.sml
@@ -173,7 +173,7 @@ in
     else
       let
         val () = diag [dir," does not exist: will clone"]
-        val status = OS.Process.system (String.concat[git_path," clone --bare --no-tags ",options,remote," ",dir])
+        val status = OS.Process.system (String.concat[git_path," clone --bare ",options,remote," ",dir])
       in
         assert (OS.Process.isSuccess status) ["git clone failed for ",dir]
       end