diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-11 14:27:46 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
commit | 2d66c7d508f6bd198969012241082e34a5b6047c (patch) | |
tree | 33b632f3118c8166a05211aa5a05375268fb78a3 /stm/spawned.ml | |
parent | 433f0bc4e5110db09c770022b277c419f8b35f64 (diff) |
CThread: use a different type for thread friendly in_channels
Diffstat (limited to 'stm/spawned.ml')
-rw-r--r-- | stm/spawned.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml index d02594569..21902f71d 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -31,6 +31,7 @@ let open_bin_connection h p = let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in set_binary_mode_in cin true; set_binary_mode_out cout true; + let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in cin, cout let controller h p = @@ -39,7 +40,7 @@ let controller h p = let ic, oc = open_bin_connection h p in let rec loop () = try - match input_value ic with + match CThread.thread_friendly_input_value ic with | Hello _ -> prerr_endline "internal protocol error"; exit 1 | ReqDie -> prerr_endline "death sentence received"; exit 0 | ReqStats -> @@ -68,6 +69,7 @@ let init_channels () = Unix.dup2 Unix.stderr Unix.stdout; set_binary_mode_in stdin true; set_binary_mode_out stdout true; + let stdin = CThread.prepare_in_channel_for_thread_friendly_io stdin in channels := Some (stdin, stdout); in match !control_channel with |