aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/spawned.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-11 14:27:46 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commit2d66c7d508f6bd198969012241082e34a5b6047c (patch)
tree33b632f3118c8166a05211aa5a05375268fb78a3 /stm/spawned.ml
parent433f0bc4e5110db09c770022b277c419f8b35f64 (diff)
CThread: use a different type for thread friendly in_channels
Diffstat (limited to 'stm/spawned.ml')
-rw-r--r--stm/spawned.ml4
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