diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 index 7e70db6b4..5500903a9 100644 --- a/scripts/coqc.ml4 +++ b/scripts/coqc.ml4 @@ -88,6 +88,9 @@ let compile command args file = if not !keep then Sys.remove tmpfile ; match status with | _, Unix.WEXITED 0 -> () + | _, Unix.WEXITED 127 -> + Printf.printf "Cannot execute %s\n" command; + exit 1 | _, Unix.WEXITED c -> exit c | _ -> exit 1 with _ -> |