diff options
| author | Enrico Tassi | 2014-01-29 23:08:45 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-30 17:29:33 +0100 |
| commit | 8c4b6ebb338c8a61c607782908254aadead0c3cd (patch) | |
| tree | 2cf4c79b5911c1853bcdd16cbe6d9ca3bab686f3 /lib/spawned.mli | |
| parent | 0a61e18a60fe05b989c24f28c769c3b0cd296cf1 (diff) | |
Work around for bug in threads + blocking io streamlined
Diffstat (limited to 'lib/spawned.mli')
| -rw-r--r-- | lib/spawned.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/spawned.mli b/lib/spawned.mli index bc5649a2fa..18b88dc64b 100644 --- a/lib/spawned.mli +++ b/lib/spawned.mli @@ -20,7 +20,3 @@ val init_channels : unit -> unit (* Once initialized, these are the channels to talk with our master *) val get_channels : unit -> in_channel * out_channel -(* In multi threaded environments on windows blocking calls do - prevent context switch. This seems a huge BUG, here a work around *) -val prepare_in_channel_for_thread_friendly_blocking_input : in_channel -> unit -val thread_friendly_blocking_input : in_channel -> string -> int -> int |