diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:14:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:24:10 +0200 |
| commit | 34a2f9eb315da8b794f2573bdfc8ff941d81bdbe (patch) | |
| tree | 06bab4b7e95d04270d0cfa52c964aa63ac43d580 /dev/doc/translate.txt | |
| parent | 417ac448411ce924444915da8e7e6fb81a12bc57 (diff) | |
Configure: viewing compilation in -local itself as an installation layout.
Consequence: docdir is always defined, no more "" in external
preferences for manual and stdlib when using coqide in -local mode.
Diffstat (limited to 'dev/doc/translate.txt')
0 files changed, 0 insertions, 0 deletions