diff options
Diffstat (limited to 'otherlibs/threads/threadUnix.mli')
| -rw-r--r-- | otherlibs/threads/threadUnix.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/otherlibs/threads/threadUnix.mli b/otherlibs/threads/threadUnix.mli index d878dece8..973d2d49f 100644 --- a/otherlibs/threads/threadUnix.mli +++ b/otherlibs/threads/threadUnix.mli @@ -49,13 +49,6 @@ val select : Unix.file_descr list -> float -> Unix.file_descr list * Unix.file_descr list * Unix.file_descr list -(*** 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 and redirections *) val pipe : unit -> Unix.file_descr * Unix.file_descr |