aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.mli')
-rw-r--r--library/library.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/library/library.mli b/library/library.mli
index bfcc04eb9..1e2197409 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -64,6 +64,7 @@ val get_full_load_paths : unit -> (System.physical_path * dir_path) list
val add_load_path : System.physical_path * dir_path -> unit
val remove_load_path : System.physical_path -> unit
val find_logical_path : System.physical_path -> dir_path
+val is_in_load_paths : System.physical_path -> bool
val load_paths_of_dir_path : dir_path -> System.physical_path list
(*s Locate a library in the load paths *)