diff options
Diffstat (limited to 'otherlibs/threads/threadUnix.ml')
| -rw-r--r-- | otherlibs/threads/threadUnix.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/otherlibs/threads/threadUnix.ml b/otherlibs/threads/threadUnix.ml index 7a4f1f3db..a136ab23c 100644 --- a/otherlibs/threads/threadUnix.ml +++ b/otherlibs/threads/threadUnix.ml @@ -70,13 +70,6 @@ let timed_write fd buff ofs len timeout = let select = Thread.select -(*** Interfacing with the standard input/output library *) - -external in_channel_of_descr : Unix.file_descr -> in_channel - = "open_descriptor" -external out_channel_of_descr : Unix.file_descr -> out_channel - = "open_descriptor" - (*** Pipes *) let pipe() = |