diff options
| author | Emilio Jesus Gallego Arias | 2016-12-06 17:16:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:47:14 +0100 |
| commit | f0341076aa60a84177a6b46db0d8d50df220536b (patch) | |
| tree | 3dd3acd080d858e7b4d14ea31231b09c8ec74ec5 /toplevel | |
| parent | eb68e001f2ebbf09dc32c999e9c9b0f116c0a530 (diff) | |
[error] Move back fatal_error to toplevel
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0ece0b0148..541c1fd1bb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -431,6 +431,13 @@ let get_native_name s = Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error info anomaly = + let msg = info ++ fnl () in + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; + exit (if anomaly then 129 else 1) + let parse_args arglist = let args = ref arglist in let extras = ref [] in |