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 /vernac | |
| parent | cfc16678b11c7be9fe24432537d830a062c33a3a (diff) | |
| parent | 250dc1f50e17240df158978159f408fe9231f410 (diff) | |
Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 *) |