diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-22 14:10:31 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-22 14:10:31 +0100 |
commit | d55676344c8dc0d9a87b2ef12ec2348281db4bf5 (patch) | |
tree | cce2b3c479ec4f9498e246b05c4b02a353fe5588 /library/library.ml | |
parent | afb9c9a65097dd901df18c443ca13ad4bf394985 (diff) |
Move the From logic to Loadpath.expand_path.
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/library/library.ml b/library/library.ml index 734a50fe3..4f964a051 100644 --- a/library/library.ml +++ b/library/library.ml @@ -297,17 +297,7 @@ let locate_absolute_library dir = let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = match root with - | None -> Loadpath.expand_path dir - | Some root -> - let filter path = - if is_dirpath_prefix_of root path then - let path = drop_dirpath_prefix root path in - is_dirpath_suffix_of dir path - else false - in - Loadpath.filter_path filter - in + let loadpath = Loadpath.expand_path ?root dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try |