X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=55029914ec12e1089f11c7af245b5fe0277ff29c;hb=3202740c95ba4b662b7f96533fccdff522e67e24;hp=d95bfdbad0a39f22b43460a6372aa6b51ee4b649;hpb=efdb0db81ef2594a2aced0310997ef0d74462254;p=helm.git

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index d95bfdbad..55029914e 100644
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -213,7 +213,6 @@ let mk_maker refresh_cb =
     try 
       let argv = Array.of_list ("make"::args) in
       pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
-let ch = open_out "/tmp/pippo" in output_string ch (String.concat " " ("make"::(Array.to_list argv)) ^ "\n"); flush ch; close_out ch;
       Unix.close out_w;
       Unix.close err_w;
       let buf = String.create 1024 in
@@ -248,7 +247,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 
@@ -278,6 +277,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