X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=6e0d5660cd62148b2cade6a99410495da25fad48;hb=52af0e3a6ab827464f33b90bf0d39e5df3169499;hp=48d6696281248cda435447c4f59a55e38936668c;hpb=afde811cd8ac8fdfebf169dfb1196493e42bbba1;p=helm.git

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 48d669628..6e0d5660c 100644
--- 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
@@ -247,7 +251,7 @@ let clean_development development =
 let clean_development_in_bg refresh_cb development =
   call_make development "clean" (mk_maker refresh_cb)
 
-let destroy_development development =
+let destroy_development_aux development clean_development =
   let delete_development development = 
     let unlink file =
       try 
@@ -277,6 +281,12 @@ let destroy_development development =
       logger `Warning "This may cause garbage."
     end;
   delete_development development 
+ 
+let destroy_development development = 
+  destroy_development_aux development clean_development
+
+let destroy_development_in_bg refresh development = 
+  destroy_development_aux development (clean_development_in_bg refresh) 
   
 let root_for_development development = development.root
 let name_for_development development = development.name