aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/control.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/control.ml b/lib/control.ml
index cce9d3a9f..04d176092 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -41,7 +41,7 @@ let unix_timeout n f e =
with e ->
let e = Backtrace.add_backtrace e in
restore_timeout ();
- raise e
+ Exninfo.iraise e
let windows_timeout n f e =
let killed = ref false in
@@ -78,7 +78,7 @@ let windows_timeout n f e =
| e ->
let () = killed := true in
let e = Backtrace.add_backtrace e in
- raise e
+ Exninfo.iraise e
type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }