diff options
| -rw-r--r-- | kernel/nativelib.ml | 5 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 1 |
2 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4e7d6b218..1e35f6c03 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 = diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index d328ad0cf..fc3495796 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -32,6 +32,7 @@ let explain_exn_default = function | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") + | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) | Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Exceptions with pre-evaluated error messages *) |