aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-08 11:36:44 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-09 13:11:38 +0200
commit4d601a87b775529b7d516fa213c688b6ecf5246d (patch)
tree0f6f2c716f3bbb8cf25032b30e4af42a223ded69 /lib/system.mli
parent938dd9ba81d0bba5a9358627405d3110fc4ee335 (diff)
toploop plugins taken into account when printing --help (close: 3535)
E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
Diffstat (limited to 'lib/system.mli')
-rw-r--r--lib/system.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/lib/system.mli b/lib/system.mli
index af797121a..e4f344f6b 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -19,7 +19,10 @@ 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
-val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
+val where_in_path :
+ ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
+val where_in_path_rex :
+ CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
val exists_dir : string -> bool