diff options
| author | sacerdot | 2000-11-29 13:54:50 +0000 |
|---|---|---|
| committer | sacerdot | 2000-11-29 13:54:50 +0000 |
| commit | 9591a484ae0e316b879f812591f457bf6edc68b2 (patch) | |
| tree | ab3ef63b504e92236ac067b21916175556b75e61 /lib | |
| parent | 72a492aca3548056d225a846fad5fcf3e1a0efba (diff) | |
load_path_entry structure simplified; field relative_subdir renamed to coq_dirpa
th
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1023 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 7 | ||||
| -rw-r--r-- | lib/system.mli | 3 |
2 files changed, 4 insertions, 6 deletions
diff --git a/lib/system.ml b/lib/system.ml index f571b4638c..bc55c461b7 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -10,8 +10,7 @@ open Unix type load_path_entry = { directory : string; - root_dir : string; - relative_subdir : string list } + coq_dirpath : string list } type load_path = load_path_entry list @@ -21,7 +20,7 @@ let exists_dir dir = let all_subdirs root alias = let l = ref [] in let add f rel = - l := { directory = f; root_dir = root; relative_subdir = rel } :: !l + l := { directory = f; coq_dirpath = rel } :: !l in let rec traverse dir rel = let dirh = opendir dir in @@ -78,7 +77,7 @@ let find_file_in_path paths name = let globname = glob name in if not (Filename.is_relative globname) then let root = Filename.dirname globname in - { directory = root; root_dir = root; relative_subdir = [] }, globname + { directory = root; coq_dirpath = [] }, globname else try search_in_path paths name diff --git a/lib/system.mli b/lib/system.mli index eb07830525..71dff73c3b 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -7,8 +7,7 @@ type load_path_entry = { directory : string; - root_dir : string; - relative_subdir : string list } + coq_dirpath : string list } type load_path = load_path_entry list |