diff options
Diffstat (limited to 'otherlibs/threads/threadUnix.mli')
| -rw-r--r-- | otherlibs/threads/threadUnix.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/otherlibs/threads/threadUnix.mli b/otherlibs/threads/threadUnix.mli index 2383c35c4..f8e37c7f9 100644 --- a/otherlibs/threads/threadUnix.mli +++ b/otherlibs/threads/threadUnix.mli @@ -57,8 +57,11 @@ val select : (*** Pipes and redirections *) val pipe : unit -> Unix.file_descr * Unix.file_descr +val open_process_in: string -> in_channel val open_process_out: string -> out_channel val open_process: string -> in_channel * out_channel +val open_process_full: + string -> env:string array -> in_channel * out_channel * in_channel (*** Time *) |