fixed matitamake to handle development with names with spaces

[helm.git] / helm / matita / matitamakeLib.ml

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 55029914ec12e1089f11c7af245b5fe0277ff29c..6e0d5660cd62148b2cade6a99410495da25fad48 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -134,6 +134,7 @@ let rebuild_makefile development =
   
 (* creates a new development if possible *)
 let initialize_development name dir =
+  let name = Pcre.replace ~pat:" " ~templ:"_" name in 
   let dev = {name = name ; root = dir} in
   match development_for_dir dir with
   | Some d ->
@@ -154,7 +155,10 @@ let make chdir args =
   let old = Unix.getcwd () in
   try
     Unix.chdir chdir;
-    let rc = Unix.system (String.concat " " ("make"::args)) in
+    let rc = 
+      Unix.system 
+        (String.concat " " ("make"::(List.map Filename.quote args)))
+    in
     Unix.chdir old;
     match rc with
     | Unix.WEXITED 0 -> true