aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-15 13:30:51 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-15 13:30:51 +0000
commit17a540b2a911927ed26190ca8a0b28efccab3bb3 (patch)
tree4a162b9e67893b49151a0669964e90d12a5c1a78 /lib
parentb2c9129662f55eea46a8937f9fd0cfabc029457a (diff)
Changed the semantics of AddRecPath.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index a967ed191..55c77b076 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -39,7 +39,12 @@ let all_subdirs root =
with End_of_file ->
closedir dirh
in
- if exists_dir root then traverse root "";
+ if exists_dir root then
+ begin
+ let root_base_name = Filename.basename root in
+ add root root_base_name ;
+ traverse root root_base_name
+ end ;
List.rev !l
let safe_getenv_def var def =