diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-06 03:42:42 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-06 03:42:42 +0000 |
| commit | 6ccc690a6e3e1754392683afd8e4086c49441942 (patch) | |
| tree | c6bf498904dcd1f3d497a993d11af6695e78086b /dev/doc/build-system.txt | |
| parent | a353947b5c7645ccc6576bad0124ef6cca358001 (diff) | |
Use $(COQTOPEXE) to refer to bin/coqtop in Makefiles
The environment variable COQTOP has a different meaning for Coq
executables and for Coq Makefiles, which is troublesome when make
forwards it to subprocesses via the environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11366 85f007b7-540e-0410-9357-904b9bb8a0f7
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 c9571f7c9..9362aeeb3 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 |