diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-12 03:47:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 12:12:56 +0200 |
| commit | 66b98ecd41bac232bbee19a9b3484feefd71df3c (patch) | |
| tree | d915918df14661fbd013071497743ce087e5e995 /ide | |
| parent | 58935ddbaf6f0e2470716d30f70ea18a9f8151c4 (diff) | |
Generalizing to docdir and datadir the test for a relocated installation.
Also standardizing the choice of the default datadir (I don't see why
we should add by default both /usr/local/share/coq and /usr/share/coq
when we know that the installation is in only one of them).
Open question: test for possible relocation of the installed coq
should be done on raw dirname of the executable or on the
standardization of this name wrt symbolic links?
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions