From 250dc1f50e17240df158978159f408fe9231f410 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 9 Feb 2018 23:33:48 +0100
Subject: [nativecomp] Remove ad-hoc handling of Dynlink exception.

Instead, we properly register a printer for such exception and update
the code.
---
 kernel/nativelib.ml  | 5 ++---
 vernac/explainErr.ml | 1 +
 2 files changed, 3 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 =
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index d328ad0cf8..fc34957968 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 *)
-- 
cgit v1.2.3