diff options
Diffstat (limited to 'library/loadpath.ml')
| -rw-r--r-- | library/loadpath.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index 26af809e7..d35dca212 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -112,3 +112,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 = get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname |