matitac now automatically cleans a non empty baseuri

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

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 2b3a4b394cbaf6b3e6215c39c214526c7853123e..534f2dc7383acba7ad01bac7a2b11dd3334112d3 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -225,6 +225,8 @@ let mk_maker refresh_cb =
       let rec aux = function 
         | f::tl ->
             let len = Unix.read f buf 0 1024 in
+            if len = 0 then 
+              raise CHILD_DEAD;
             vt100 (String.sub buf 0 len);
             aux tl
         | _ -> ()
@@ -236,12 +238,9 @@ let mk_maker refresh_cb =
       done;
       true
     with CHILD_DEAD -> 
+      ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
       let _, status = Unix.waitpid [] !pid in
-      match status with
-      | Unix.WEXITED 0 -> 
-          ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
-          true
-      | _ -> false)
+      match status with | Unix.WEXITED 0 -> true | _ -> false)
   
 
 let build_development_in_bg ?(target="all") refresh_cb development =