aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.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/libnames.ml
parentafb9c9a65097dd901df18c443ca13ad4bf394985 (diff)
Move the From logic to Loadpath.expand_path.
Diffstat (limited to 'library/libnames.ml')
0 files changed, 0 insertions, 0 deletions