aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-04 11:25:51 +0100
committerPierre-Marie Pédrot2020-03-04 11:25:51 +0100
commit89f111f2e15d8cab61495a419f0c9f7ae95e086a (patch)
tree300ebf99c79fe0e91faf2ad50439b17916e60cf7 /lib/system.ml
parent2937fe5c1bb14a7cb7f00bb6e8d418ece00a7f50 (diff)
parentb2c58a23a1f71c86d8a64147923214b5059bd747 (diff)
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
Reviewed-by: Matafou Reviewed-by: ppedrot
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 2d68fd2fdf..9089eda564 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -248,9 +248,9 @@ let extern_state magic filename val_0 =
marshal_out channel val_0;
close_out channel
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = try_remove filename in
- iraise reraise
+ Exninfo.iraise reraise
with Sys_error s ->
CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s)