diff options
author | 2008-09-08 00:15:04 +0200 | |
---|---|---|
committer | 2008-09-08 00:16:06 +0200 | |
commit | 5c6894942e4de978963144606e89db432c306625 (patch) | |
tree | a8f1fe2e658c9ba460f1c9af99393d9af21b2dfd /dev/doc/build-system.txt | |
parent | 745e0fb3b3bc4c435870f1af25c22d495fac9f29 (diff) | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Merge commit 'upstream/8.2.beta4.svn20080907+dfsg'
Diffstat (limited to 'dev/doc/build-system.txt')
-rw-r--r-- | dev/doc/build-system.txt | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index c9571f7c..9362aeeb 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -253,9 +253,8 @@ config/Makefile looks like it contains a lot of unused variables, clean that up (are any maybe used by nightly scripts on pauillac?). Also, the COQTOP variable from config/Makefile (and used in contribs) has a very poorly chosen name, because "coqtop" is the -name of a Coq executable! For example, in the Coq makefile it is -immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or -COQTREE or COQDIR or ... +name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used +to refer to that executable. Promote the granular .glob handling to official way of doing things for Coq developments, that is implement it in coq_makefile and the |