aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-17 12:28:46 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-10-10 14:05:54 +0200
commit7c36b13fdc6412450de6face4df18aea9d9bbaac (patch)
tree8975af385eea59e829c1c04d11e95d20ab81fd0f /config
parent3a3ec7e1f306a49008edf47476ea5fb410233b95 (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