diff options
| author | Emilio Jesus Gallego Arias | 2020-01-08 20:14:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-03 16:54:16 -0500 |
| commit | b2c58a23a1f71c86d8a64147923214b5059bd747 (patch) | |
| tree | ea91b763facc24df188bd481b7a60e238f7a60a2 /kernel/nativelib.ml | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
[exninfo] Deprecate aliases for exception re-raising.
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 86eaaddc90..3f2e63b984 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -180,8 +180,8 @@ let call_linker ?(fatal=true) env ~prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error _ as exn -> - let exn = CErrors.push exn in - if fatal then iraise exn + let exn = Exninfo.capture exn in + if fatal then Exninfo.iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () |