diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-01 18:31:05 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:13 +0100 |
commit | 14155762a7cd46ed6a3e9cf2a58e11ee1244b188 (patch) | |
tree | 27d17f64dae70cb2e75828b6a22c66db6451d573 /lib/cErrors.ml | |
parent | 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 (diff) |
[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
Diffstat (limited to 'lib/cErrors.ml')
-rw-r--r-- | lib/cErrors.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index dbebe6a48..9cbc3fb6d 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -22,7 +22,7 @@ exception Anomaly of string option * std_ppcmds (* System errors *) * Anyways, tagging should not happen here, but in the specific * listener to the msg_* stuff. *) -let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc () +let tag_err_str s = tag Ppstyle.error_tag (str s) ++ spc () let err_str = tag_err_str "Error:" let ann_str = tag_err_str "Anomaly:" @@ -154,6 +154,6 @@ let handled e = let fatal_error info anomaly = let msg = info ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; + pp_with !Pp_control.err_ft msg; Format.pp_print_flush !Pp_control.err_ft (); exit (if anomaly then 129 else 1) |