diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:11:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:21:21 +0200 |
| commit | 417ac448411ce924444915da8e7e6fb81a12bc57 (patch) | |
| tree | f9ab75068617f0c0a598e058da206803883d0103 /dev/doc | |
| parent | 168bb8fd5fe62beebd5e4998e903777b33654a4a (diff) | |
Configuration: always giving a value to configdir and datadir.
They were not used for looking for coqide files in the situation when
the effective installation path happens to be exactly the installation
path proposed by default, while relevant files were however (possibly)
installed in these directories.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions