X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=8dc45faaaff1d75877d93d83ac699b3e42303a4f;hb=7c0db1e564918026d56e81163b4f1e4aee649055;hp=2b3a4b394cbaf6b3e6215c39c214526c7853123e;hpb=ecd0ab19b82f611974bd76f3c740c842f566009d;p=helm.git

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 2b3a4b394..8dc45faaa 100644
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -175,8 +175,6 @@ let call_make development target make =
 let build_development ?(target="all") development =
   call_make development target make
 
-exception CHILD_DEAD
-  
 (* not really good vt100 *)
 let vt100 s =
   let rex = Pcre.regexp "\\[[0-9;]+m" in
@@ -213,10 +211,8 @@ let mk_maker refresh_cb =
     let out_r,out_w = Unix.pipe () in
     let err_r,err_w = Unix.pipe () in
     let pid = ref ~-1 in
+    ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
     try 
-      let _ = 
-        Sys.signal Sys.sigchld (Sys.Signal_handle (fun _ -> raise CHILD_DEAD))
-      in
       let argv = Array.of_list ("make"::args) in
       pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
       Unix.close out_w;
@@ -225,6 +221,10 @@ 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 
+                (Unix.Unix_error 
+                  (Unix.EPIPE,"read","len = 0 (matita internal)"));
             vt100 (String.sub buf 0 len);
             aux tl
         | _ -> ()
@@ -235,14 +235,9 @@ let mk_maker refresh_cb =
         refresh_cb ()
       done;
       true
-    with CHILD_DEAD -> 
-      let _, status = Unix.waitpid [] !pid in
-      match status with
-      | Unix.WEXITED 0 -> 
-          ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
-          true
-      | _ -> false)
-  
+    with 
+    | Unix.Unix_error (_,"read",_)
+    | Unix.Unix_error (_,"select",_) -> true)
 
 let build_development_in_bg ?(target="all") refresh_cb development =
   call_make development target (mk_maker refresh_cb)