aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.mli
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 11:21:42 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 11:21:42 +0100
commitafb9c9a65097dd901df18c443ca13ad4bf394985 (patch)
treef1436684288cfcd7db59f1b1e1cf3b2e743af38f /library/loadpath.mli
parent8c51055e67da3fea8b66ebcff6c82cbea079dcee (diff)
Do not query module files that have already been loaded.
For a script that does just "Require Reals", this avoids 40k queries. Note that this changes the signature of the FileDependency feedback. Indeed, it no longer provides the physical path to the dependency but only its logical path (since the physical path is no longer available). The physical path could still have been recovered thanks to the libraries_filename_table list. But due to the existence of the overwrite_library_filenames function, its content cannot be trusted. So anyone interested in the actual physical path should now also rely on the FileLoaded feedback.
Diffstat (limited to 'library/loadpath.mli')
0 files changed, 0 insertions, 0 deletions