diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-08 17:04:43 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-08 17:04:43 +0200 |
| commit | ef3f9fac7cff820bd927d122caef2c37a68a55c8 (patch) | |
| tree | 4f0edc4bab216df032f30d42261f407bb28b405a /plugins/micromega/mutils.ml | |
| parent | 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (diff) | |
Avoid canonizing the same paths over and over.
The number of path canonizations was quadratic in the number of potential
plugin directories. This patch makes it linear; on a standard Coq tree,
this brings the number of chdir and getcwd system calls from more than
1,000 down to about 200 at startup.
This also fixes a bug where the Cd vernacular command could cause plugins
to break since relative paths were used to locate them.
Diffstat (limited to 'plugins/micromega/mutils.ml')
0 files changed, 0 insertions, 0 deletions