Réparation de bugs de LoadPath

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

1 files changed, 7 insertions, 5 deletions

diff --git a/library/library.ml b/library/library.ml
index f2468d32d..6839bdb9c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -20,11 +20,11 @@ let add_load_path_entry lpe = load_path := lpe :: !load_path
 let add_path dir coq_dirpath = 
   if coq_dirpath = [] then anomaly "add_path: empty path in library";
   Nametab.push_library_root (List.hd coq_dirpath);
-  if (Unix.stat dir).Unix.st_kind = Unix.S_DIR then
-   add_load_path_entry
-     { directory = dir; coq_dirpath = coq_dirpath }
+  if exists_dir dir then
+    add_load_path_entry { directory = dir; coq_dirpath = coq_dirpath }
   else
-   error (dir ^ " is not an existant directory")
+    wARNING [< 'sTR ("Cannot open " ^ dir) >]
+
 
 let remove_path dir =
   load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
@@ -32,7 +32,9 @@ let remove_path dir =
 let rec_add_path dir coq_dirpath =
   if coq_dirpath = [] then anomaly "add_path: empty path in library";
   Nametab.push_library_root (List.hd coq_dirpath);
-  load_path := (all_subdirs dir (Some coq_dirpath)) @ !load_path
+  let dirs = all_subdirs dir (Some coq_dirpath) in
+  if dirs = [] then wARNING [< 'sTR ("Cannot open " ^ dir) >];
+  load_path := dirs @ !load_path
 
 (*s Modules on disk contain the following informations (after the magic 
     number, and before the digest). *)