do not explode if a plugin is not up to date on -help (Close: 3673)

1 files changed, 4 insertions, 1 deletions

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index c609a6e241..d9b739354e 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -314,7 +314,10 @@ let dir_ml_load m = ignore(dir_ml_load m)
 let add_known_module m = add_known_module m None
 let load_ml_object_raw fname = dir_ml_load (file_of_name fname)
 let load_ml_objects_raw_rex rex =
-  List.iter (fun (_,fp) -> dir_ml_load (file_of_name (Filename.basename fp)))
+  List.iter (fun (_,fp) ->
+    let name = file_of_name (Filename.basename fp) in
+    try dir_ml_load name
+    with e -> prerr_endline (Printexc.to_string e))
     (System.where_in_path_rex !coq_mlpath_copy rex)
 
 (* Summary of declared ML Modules *)