aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cErrors.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-01 18:31:05 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 15:47:13 +0100
commit14155762a7cd46ed6a3e9cf2a58e11ee1244b188 (patch)
tree27d17f64dae70cb2e75828b6a22c66db6451d573 /lib/cErrors.ml
parent8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 (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.ml4
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)