diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 04:59:20 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-08 02:27:48 -0400 |
| commit | 909160efe42ef1f2cb7f559e3cb5039a9680ca6c (patch) | |
| tree | 142f72ebab2bd39f77ace2b54ace50a8edc6de49 /lib | |
| parent | b26d1f477990d88e235ffda0f23f494456ce5862 (diff) | |
[errors] Print backtrace of internal errors in printers
This is useful as witnessed by #11829 , as some errors printers do
still fail, so it costs little to have both backtraces.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 4 |
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) = |