Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules

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

1 files changed, 2 insertions, 3 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 55c77b076..5da2d9f35 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -41,9 +41,8 @@ let all_subdirs root =
   in
   if exists_dir root then
    begin
-    let root_base_name = Filename.basename root in
-     add root root_base_name ;
-     traverse root root_base_name
+     add root "";
+     traverse root ""
    end ;
   List.rev !l