aboutsummaryrefslogtreecommitdiff
path: root/library/loadpath.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-10-02 16:01:46 +0200
committerPierre-Marie Pédrot2015-10-02 16:01:46 +0200
commit16c88c9be5c37ee2e4fe04f7342365964031e7dd (patch)
tree7b5c07362dad323acae516718b9cebe94bd639af /library/loadpath.ml
parenta3d7630d74b720b771e880dcf0fcad05de553a6e (diff)
parent88abc50ece70405d71777d5350ca2fa70c1ff437 (diff)
Merge branch 'v8.5'
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 26af809e78..622d390a2c 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