summaryrefslogtreecommitdiff
path: root/library/loadpath.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
commit4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch)
treeaefad2e3de35f75c46729f9310d33b56d3821961 /library/loadpath.ml
parent64fa31c7ee53e79b112507fb2eea27dc7648328d (diff)
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'library/loadpath.ml')
-rw-r--r--library/loadpath.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e..622d390a 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -28,8 +28,6 @@ let physical p = p.path_physical
let get_load_paths () = !load_paths
-let get_paths () = List.map physical !load_paths
-
let anomaly_too_many_paths path =
anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
@@ -112,3 +110,9 @@ let expand_path dir =
if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
in
aux !load_paths
+
+let locate_file fname =
+ let paths = List.map physical !load_paths in
+ let _,longfname =
+ System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+ longfname