diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-10 20:27:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:15:31 +0200 |
| commit | 96ec7b5e65f79118914b7c81e14587d0dc065cc1 (patch) | |
| tree | 6998b6515ea3495c4de0715a3b60a70f60033b3e /doc | |
| parent | 25020ba614315ce143f657511696fb7bf5135b00 (diff) | |
Mini-renaming in configure.ml to avoid switching back and forth from
"libdir" to "COQLIBINSTALL" then "libdir", then "coqlib".
For the record, here is how installation options are named at the
current time in the different places they are used (if any):
Name in Name in Name in Name of option Name in Name of option
config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep
--------------------------------------------------------------------------------------------------------
COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib
DOCDIR DOCDIR docdir -docdir docdir
CONFIGDIR configdir -configdir
DATADIR datadir -datadir
BINDIR -bindir
MANDIR -mandir
EMACSLIB -emacslib
COQDOCDIR -coqdocdir
Note: in envars.ml, docdir and coqlib are recomputed
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions