diff options
Diffstat (limited to 'otherlibs/unix/unix.ml')
| -rw-r--r-- | otherlibs/unix/unix.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/unix/unix.ml b/otherlibs/unix/unix.ml index e9f96e10e..85919c32b 100644 --- a/otherlibs/unix/unix.ml +++ b/otherlibs/unix/unix.ml @@ -648,6 +648,6 @@ let establish_server server_fun sockaddr = server_fun inchan outchan; close_in inchan; close_out outchan - | id -> close s; waitpid [] id (* Reclaim the son *); () + | id -> close s; let _ = waitpid [] id (* Reclaim the son *) in () done |