little bug in coercion generation found. it use to create more coercions that expecte...

[helm.git] / matita / matitamakeLib.ml

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index 4544f9ada5c6f99ebeb23131609b1103d433f584..0ab251ddc5d3c5784f2a296550e767f5f4219dc1 100644 (file)
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -193,11 +193,7 @@ let call_make ?matita_flags development target make =
   let csc = try ["SRC=" ^ Sys.getenv "SRC"] with Not_found -> [] in
   rebuild_makefile development;
   let makefile = makefile_for_development development in
-  let nodb =
-    Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb"
-  in
   let flags = [] in 
-  let flags = flags @ if nodb then ["NODB=true"] else [] in
   let flags =
     try
       flags @ [ sprintf "MATITA_FLAGS=\"%s\"" matita_flags ]
@@ -247,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
@@ -271,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)