aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-04-09 13:26:57 +0200
committerPierre-Marie Pédrot2020-04-09 13:26:57 +0200
commita172d9e249c4e59b957c8afbfa352af525f4607d (patch)
tree02820cecb16c34b17748e4ba4c7b631eb7d8492d
parent75589e466c9f0ed62dd10fff6c1f7d284c7ffa89 (diff)
parent909160efe42ef1f2cb7f559e3cb5039a9680ca6c (diff)
Merge PR #12046: [errors] Print backtrace of internal errors in printers
Reviewed-by: ppedrot
-rw-r--r--lib/cErrors.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index d1548ab12e..62d465c703 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -106,8 +106,10 @@ let print_gen ~anomaly (e, info) =
try
print_gen ~anomaly ~extra_msg !handle_stack e
with exn ->
+ let exn, info = Exninfo.capture exn in
(* exception in error printer *)
- str "<in exception printer>" ++ fnl () ++ print_anomaly anomaly exn
+ str "<in exception printer>:" ++ print_backtrace info ++
+ str "<original exception:" ++ print_anomaly anomaly exn
(** The standard exception printer *)
let iprint (e, info) =