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. --- vernac/explainErr.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'vernac/explainErr.ml') 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 *) -- cgit v1.2.3