aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-20 12:27:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-20 13:17:15 +0200
commitfd13e21ccb89e2fa3a80074f9d7afd8b0638fdcb (patch)
treea690713016555ca6d1e9cfe98638d5193f90fdd8 /lib
parent969e77f88fe2c9d766cd2cf6e6fd7d08719a7cb7 (diff)
Adding an OCaml printer for pre-initialization anomalies.
Diffstat (limited to 'lib')
-rw-r--r--lib/errors.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/errors.ml b/lib/errors.ml
index c1d224dfc..8982dde14 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -16,6 +16,13 @@ let push = Backtrace.add_backtrace
exception Anomaly of string option * std_ppcmds (* System errors *)
+let _ =
+ let pr = function
+ | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
+ | _ -> None
+ in
+ Printexc.register_printer pr
+
let make_anomaly ?label pp =
Anomaly (label, pp)