diff options
| author | Pierre-Marie Pédrot | 2019-04-11 10:12:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-11 10:12:49 +0200 |
| commit | 36c15766a9295d980d142da0e42aebf1309f4eb4 (patch) | |
| tree | aa60444139ed57aa969389eea9ccbf1ebedf4ea0 /tools | |
| parent | ddf6dffe7d9afe635d32c41336345812f7c71139 (diff) | |
| parent | 78259a079da05b691d0cad87c70a446568427697 (diff) | |
Merge PR #9938: [coqdep] Exit with error code on exception.
Reviewed-by: ppedrot
Diffstat (limited to 'tools')
| -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 |