diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-17 12:28:46 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-10 14:05:54 +0200 |
commit | 7c36b13fdc6412450de6face4df18aea9d9bbaac (patch) | |
tree | 8975af385eea59e829c1c04d11e95d20ab81fd0f /config | |
parent | 3a3ec7e1f306a49008edf47476ea5fb410233b95 (diff) |
Restoring test on ident validity while browsing directory structure.
The test was abandoned at the time of merging subdirectory browsing
between coqdep and coqtop, and to limit at the same time the
dependency of coqdep in files such as unicode.cmo.
But checking ident validity speeds up browsing in arbitrary directory
structure and we restore it for this reason.
(One could also say that browsing arbitrary directory structures is
not intended, but in practice this may happen, as e.g. reported in
BZ#5734.)
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions