On ignore les répertoires qui ne correspondent pas à des idents

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2016 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 2 deletions

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 3e97b30f7..be6d057b9 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -157,11 +157,19 @@ let add_path dir coq_dirpath =
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
+let convert_string d =
+  try Names.id_of_string d
+  with _ -> 
+    if_verbose warning 
+      ("Directory "^d^" cannot be used as a Coq identifier (skipped)");
+    flush_all ();
+    failwith "caught"
+
 let add_rec_path dir coq_dirpath =
   let dirs = all_subdirs dir in
   if dirs <> [] then
-    let convert = List.map Names.id_of_string in
-    let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
+    let convert_dirs (lp,cp) = (lp,coq_dirpath@(List.map convert_string cp)) in
+    let dirs = map_succeed convert_dirs dirs in
     begin
       List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
       List.iter Library.add_load_path_entry dirs;