aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-04-01 10:51:32 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-04-01 16:38:41 +0200
commit7c41bc9bdc883aacbc015954a89ff13fe9c9c1c0 (patch)
tree573d4063c5d35fa318178bd9215b0c10a31ff157 /library/loadpath.mli
parent569cf23a28c344fe32bd4e9712a4e2028c350de2 (diff)
From X Require Y looks for X with absolute path, disregarding -R.
Diffstat (limited to 'library/loadpath.mli')
-rw-r--r--library/loadpath.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/library/loadpath.mli b/library/loadpath.mli
index ae54b3183..3251b8c60 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -49,5 +49,6 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
(** Given a relative logical path, associate the list of absolute physical and
logical paths which are possible matches of it. *)
-val expand_root_path : DirPath.t -> CUnix.physical_path list
-(** As [expand_path] but ignores the implicit status. *)
+val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
+(** As {!expand_path} but uses a filter function instead, and ignores the
+ implicit status of loadpaths. *)