diff options
| author | Emilio Jesus Gallego Arias | 2020-01-16 19:57:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-16 20:00:03 +0100 |
| commit | cd7052d68fb1bd56c4c1182a47b180b992abd5e0 (patch) | |
| tree | 74c29dc6f12c0cc08caa2d0f1348f5707ec1a69d /vernac/himsg.ml | |
| parent | 404a24241e3ff89994aa48524d2b34dcb4773300 (diff) | |
[mltop] Remove error handling hacks in favor of default methods.
We don't need to handle `Dynlink` errors specially anymore.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba7ae5069b..eb39564fed 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1364,7 +1364,6 @@ let explain_exn_default = function | Sys_error msg -> hov 0 (str "System error: " ++ quote (str 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)) | CErrors.Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Otherwise, not handled here *) |