diff options
Diffstat (limited to 'vernac/mltop.ml')
| -rw-r--r-- | vernac/mltop.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index ab9d008659..5046248e11 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -99,9 +99,9 @@ let ocaml_toploop () = *) let _ = CErrors.register_handler (function | Dynlink.Error e -> - hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) + Some (hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))) | _ -> - raise CErrors.Unhandled + None ) let ml_load s = |