diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-22 11:21:42 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-22 11:21:42 +0100 |
commit | afb9c9a65097dd901df18c443ca13ad4bf394985 (patch) | |
tree | f1436684288cfcd7db59f1b1e1cf3b2e743af38f /library/loadpath.mli | |
parent | 8c51055e67da3fea8b66ebcff6c82cbea079dcee (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