From 76ae754c2724974aeb81855f2cf54f342e69a519 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 24 Sep 2020 19:11:20 +0200
Subject: [PATCH] [Kernel] Keep the backtrace with the exception
---
src/libraries/utils/command.ml | 8 +++++---
src/libraries/utils/command.mli | 2 +-
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 22ab26bbb6a..f51fc989837 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -111,11 +111,13 @@ let print_file file job =
(* -------------------------------------------------------------------------- *)
type timer = float ref
-type 'a result = Result of 'a | Error of exn
+type 'a result = Result of 'a | Error of Printexc.raw_backtrace * exn
let dt_max tm dt = match tm with Some r when dt > !r -> r := dt | _ -> ()
let dt_add tm dt = match tm with Some r -> r := !r +. dt | _ -> ()
-let return = function Result x -> x | Error e -> raise e
-let catch f x = try Result(f x) with e -> Error e
+let return = function Result x -> x | Error (bt,e) -> Printexc.raise_with_backtrace e bt
+let catch f x = try Result(f x) with e ->
+ let bt = Printexc.get_raw_backtrace () in
+ Error (bt,e)
let time ?rmax ?radd job data =
begin
let t0 = Sys.time () in
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 0643c00007d..10449cbf130 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -62,7 +62,7 @@ val print_file : string -> (Format.formatter -> 'a) -> 'a
(* ************************************************************************* *)
type timer = float ref
-type 'a result = Result of 'a | Error of exn
+type 'a result = Result of 'a | Error of Printexc.raw_backtrace * exn
val catch : ('a -> 'b) -> 'a -> 'b result
val return : 'a result -> 'a
val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b
--
GitLab