aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.mli
diff options
context:
space:
mode:
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. *)