diff options
| author | letouzey | 2012-08-23 12:52:43 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-23 12:52:43 +0000 |
| commit | 650f9c37a3ac80f1e0121f01c67889e2c55838c8 (patch) | |
| tree | 89393969a088d82347c5b4c162ab566bb03f1919 /scripts | |
| parent | 9f465647f3ad78e324d1c86559e8045855d1dea3 (diff) | |
Configure + Makefile : simplification when -local
When local=true:
- "make install" is now a no-op
- In configure, no need hence to fill the various variables
about installation (BINDIR, COQLIBINSTALL, MANDIR,
DOCDIR, EMACSLIB). This avoids many references to
absolute location of the coq sources (which may contain
blanks or other strange chars in win32).
- For the moment, we keep CONFIGDIR and DATADIR, used when
launching coqide from inside the build directory.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15749 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions