matitamake is integrated with matita

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

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 2facdda09e9b3182cdbec5c58a5f4d279d0e7771..512da157ae5cbdedfbe56b46b36a400699d31aa5 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -149,18 +149,22 @@ let initialize_development name dir =
   | None -> 
       dump_development dev;
       rebuild_makefile dev;
+      developments := dev :: !developments;
       Some dev
 
 let make chdir args = 
   let old = Unix.getcwd () in
-  Unix.chdir chdir;
-(*  prerr_endline (String.concat " " ("make"::args));*)
-  let rc = Unix.system (String.concat " " ("make"::args)) in
-  Unix.chdir old;
-  match rc with
-  | Unix.WEXITED 0 -> true
-  | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false
-  | _ -> logger `Error "make STOPPED or SIGNALED!";false
+  try
+    Unix.chdir chdir;
+    let rc = Unix.system (String.concat " " ("make"::args)) in
+    Unix.chdir old;
+    match rc with
+    | Unix.WEXITED 0 -> true
+    | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false
+    | _ -> logger `Error "make STOPPED or SIGNALED!";false
+  with Unix.Unix_error (_,cmd,err) -> 
+    logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err);
+    false
       
 let call_make development target =
   rebuild_makefile development;
@@ -195,7 +199,9 @@ let destroy_development development =
     unlink (pool () ^ development.name ^ rootfile);
     unlink (pool () ^ development.name ^ "/depend");
     unlink (pool () ^ development.name ^ "/depend.short");
-    rmdir (pool () ^ development.name)
+    rmdir (pool () ^ development.name);
+    developments := 
+      List.filter (fun d -> d.name <> development.name) !developments
   in
   if not(clean_development development) then
     begin
@@ -204,4 +210,6 @@ let destroy_development development =
     end;
   delete_development development 
   
-  
+let root_for_development development = development.root
+let name_for_development development = development.name
+