diff options
| author | Maxime Dénès | 2018-02-12 10:07:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 10:07:09 +0100 |
| commit | ab52b106915e00130ba593122595af155b7928ba (patch) | |
| tree | 2a21917c0751d8ed454ea98674aae145aaa505eb /kernel/nativelib.ml | |
| parent | cfc16678b11c7be9fe24432537d830a062c33a3a (diff) | |
| parent | 250dc1f50e17240df158978159f408fe9231f410 (diff) | |
Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4e7d6b218c..1e35f6c036 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -157,9 +157,8 @@ let call_linker ?(fatal=true) prefix f upds = register_native_file prefix with Dynlink.Error e as exn -> let exn = CErrors.push exn in - let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); + if fatal then iraise exn + else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = |