diff options
Diffstat (limited to 'lib/spawn.ml')
-rw-r--r-- | lib/spawn.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/lib/spawn.ml b/lib/spawn.ml index 47917697..63e9e452 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let proto_version = 0 let prefer_sock = Sys.os_type = "Win32" -let accept_timeout = 2.0 +let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () @@ -28,8 +30,6 @@ module type Control = sig end -module type Empty = sig end - module type MainLoopModel = sig type async_chan type condition @@ -200,7 +200,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) p, cout let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; input_value oob_resp @@ -216,7 +216,7 @@ let rec wait p = end -module Sync(T : Empty) = struct +module Sync () = struct type process = { cin : in_channel; @@ -251,7 +251,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = with e -> prerr_endline ("kill: "^Printexc.to_string e) end let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; let RespStats g = input_value oob_resp in g |