diff options
| author | Pierre-Marie Pédrot | 2020-04-27 17:15:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-27 17:28:29 +0200 |
| commit | 6334ab72d55cb93a877933bd3f56a90d859d518d (patch) | |
| tree | 13125ecba082ddd432420dc6ef51ac265333c4ba /dev | |
| parent | e0d7b05789d7c6d341d3001c227d99a278743fd1 (diff) | |
Do not delay the loading of the library_disk field when requiring libraries.
The reason for which the code was written this way is probably historical. In
the current implementation, we read the marshalled data exactly once by library,
thus there is no gain from delaying.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions