diff options
author | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 13:30:51 +0000 |
---|---|---|
committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 13:30:51 +0000 |
commit | 17a540b2a911927ed26190ca8a0b28efccab3bb3 (patch) | |
tree | 4a162b9e67893b49151a0669964e90d12a5c1a78 /lib | |
parent | b2c9129662f55eea46a8937f9fd0cfabc029457a (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.ml | 7 |
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 = |