aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 14:10:31 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 14:10:31 +0100
commitd55676344c8dc0d9a87b2ef12ec2348281db4bf5 (patch)
treecce2b3c479ec4f9498e246b05c4b02a353fe5588 /library/library.ml
parentafb9c9a65097dd901df18c443ca13ad4bf394985 (diff)
Move the From logic to Loadpath.expand_path.
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml12
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