diff options
Diffstat (limited to 'otherlibs/unix/unix.mli')
| -rw-r--r-- | otherlibs/unix/unix.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/otherlibs/unix/unix.mli b/otherlibs/unix/unix.mli index 3b48a8d41..b1a866f7a 100644 --- a/otherlibs/unix/unix.mli +++ b/otherlibs/unix/unix.mli @@ -158,8 +158,11 @@ external wait : unit -> int * process_status = "unix_wait" and termination status. *) external waitpid : wait_flag list -> int -> int * process_status = "unix_waitpid" - (* Same as [waitopt], but waits for the process whose pid is given. - Negative pid arguments represent process groups. *) + (* Same as [wait], but waits for the process whose pid is given. + A pid of [0] means wait for any child. + Negative pid arguments represent process groups. + The list of options indicates whether [waitpid] should return + immediately without waiting, or also report stopped children. *) val system : string -> process_status (* Execute the given command, wait until it terminates, and return its termination status. The string is interpreted by the shell |