diff options
| author | Emilio Jesus Gallego Arias | 2019-04-10 02:18:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-10 03:37:48 +0200 |
| commit | 78259a079da05b691d0cad87c70a446568427697 (patch) | |
| tree | 78f8e14730b55cc4cd9a7f91d627ad9d9f67fd94 /tools/coqdep.ml | |
| parent | e3e3e6949f1c80abec9942ee0d258b58e5a7d382 (diff) | |
[coqdep] Exit with error code on exception.
This turns out to confuse many tools otherwise.
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 66f1f257b8..7114965a11 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -563,4 +563,5 @@ let _ = try coqdep () with CoqlibError msg -> - eprintf "*** Error: %s@\n%!" msg + eprintf "*** Error: %s@\n%!" msg; + exit 1 |