diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 18:52:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 18:52:09 +0100 |
| commit | de8888e28ad793511ba2e2969516325b0be44330 (patch) | |
| tree | f910699eb3afb1f2b1835a01e8529c48c950b861 /lib/system.mli | |
| parent | 9daec838c8896e7c1048b42d01eba0c71c912f00 (diff) | |
Revert "Using same code for browsing physical directories in coqtop and coqdep."
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/system.mli b/lib/system.mli index 32a84f599..a3d66d577 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -14,6 +14,8 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) +val exclude_search_in_dirname : string -> unit + val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool @@ -22,6 +24,8 @@ val where_in_path : val where_in_path_rex : CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list +val exists_dir : string -> bool + val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string |