signal hadler restored after runnig external 'make'

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index df0df823a1547c3b78fb6cdb9512dde5e6b169e4..0ab251ddc5d3c5784f2a296550e767f5f4219dc1 100644 (file)
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -243,7 +243,7 @@ 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));
+    let oldhandler = Sys.signal Sys.sigchld (Sys.Signal_ignore) in
     try
 (*       prerr_endline (String.concat " " args); *)
       let argv = Array.of_list ("make"::args) in
@@ -267,10 +267,13 @@ let mk_maker refresh_cb =
         aux r;
         refresh_cb ()
       done;
+      ignore(Sys.signal Sys.sigchld oldhandler);
       true
     with 
     | Unix.Unix_error (_,"read",_)
-    | Unix.Unix_error (_,"select",_) -> true)
+    | Unix.Unix_error (_,"select",_) -> 
+        ignore(Sys.signal Sys.sigchld oldhandler);
+        true)
 
 let build_development_in_bg ?matita_flags ?(target="all") refresh_cb development =
   call_make ?matita_flags development target (mk_maker refresh_cb)