diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-10 10:12:41 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-10 10:12:41 +0100 |
| commit | 4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4 (patch) | |
| tree | b2551173c2f88d8c2e15cb30ed5978b008e6881c /driver | |
| parent | 35e3f39bf967c4ed2ba3390b488604554306065d (diff) | |
| download | compcert-4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4.tar.gz compcert-4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4.zip | |
Harden Driver.command against EINTR errors
Sometimes, Unix.waitpid returns early with a EINTR error code, e.g. if a signal was handled. (Observed while running ccomp under the lldb debugger in MacOS X). Just restart Unix.waitpid in this case.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 59e3fa3b..391af5e7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -25,6 +25,10 @@ let sdump_suffix = ref ".json" (* Invocation of external tools *) +let rec waitpid_no_intr pid = + try Unix.waitpid [] pid + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid + let command ?stdout args = if !option_v then begin eprintf "+ %s" (String.concat " " args); @@ -45,7 +49,7 @@ let command ?stdout args = let pid = Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in let (_, status) = - Unix.waitpid [] pid in + waitpid_no_intr pid in if stdout <> None then Unix.close fd_out; match status with | Unix.WEXITED rc -> rc |