summaryrefslogtreecommitdiff
path: root/library/loadpath.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /library/loadpath.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (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