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 "\e\\[[0-9;]+m" in
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;
| f::tl ->
let len = Unix.read f buf 0 1024 in
if len = 0 then
- raise CHILD_DEAD;
+ raise
+ (Unix.Unix_error
+ (Unix.EPIPE,"read","len = 0 (matita internal)"));
vt100 (String.sub buf 0 len);
aux tl
| _ -> ()
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 -> 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)