diff options
| author | glondu | 2008-09-06 03:42:42 +0000 |
|---|---|---|
| committer | glondu | 2008-09-06 03:42:42 +0000 |
| commit | 6ccc690a6e3e1754392683afd8e4086c49441942 (patch) | |
| tree | c6bf498904dcd1f3d497a993d11af6695e78086b /dev/include | |
| 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/include')
0 files changed, 0 insertions, 0 deletions