| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.)
|
|
|
|
|
| |
This refines e234f3ef. By the way, note that e234f3ef fixed #5391
(command line tools do not accept trailing "/" - or "\" - in windows).
|
| |
|
| |
|
|
|
|
|
|
| |
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
|
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|