diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-05 18:41:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-02 22:25:44 +0200 |
| commit | 07432c05d3c814ae694f4b817be5e1589b8202ff (patch) | |
| tree | e08529d454a12b8abc15c040abdfc9cc610b8660 /toplevel/coqargs.ml | |
| parent | aae89bce1ca7c1a21b7eef345050dff5a9e88748 (diff) | |
Making explicit that errors happen in one of five executation phases.
The five phases are command line interpretation, initialization,
prelude loading, rcfile loading, and sentence interpretation (only the
two latters are located).
We then parameterize the feedback handler with the given execution
phase, so as to possibly annotate the message with information
pertaining to the phase.
Diffstat (limited to 'toplevel/coqargs.ml')
| -rw-r--r-- | toplevel/coqargs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index a1a07fce8..17e848c5a 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -10,8 +10,8 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error exn = + Topfmt.print_err_exn Topfmt.ParsingCommandLine exn; let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code |