diff options
| author | sacerdot | 2000-11-15 13:30:51 +0000 |
|---|---|---|
| committer | sacerdot | 2000-11-15 13:30:51 +0000 |
| commit | 17a540b2a911927ed26190ca8a0b28efccab3bb3 (patch) | |
| tree | 4a162b9e67893b49151a0669964e90d12a5c1a78 /lib/system.ml | |
| 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/system.ml')
| -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 a967ed191c..55c77b0769 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 = |
