diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml index a05f20728d..26262a7ddb 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -85,7 +85,8 @@ let rec make_compilation_args = function let compile command args files = let args' = command :: args @ (make_compilation_args files) in - Unix.execvpe command (Array.of_list args') environment + Unix.handle_unix_error + Unix.execvpe command (Array.of_list args') environment (* parsing of the command line * |