aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorlmamane2007-07-18 16:02:26 +0000
committerlmamane2007-07-18 16:02:26 +0000
commitbc280bc068055fa8b549ce2167e064678146ea2a (patch)
treee48d3529811cbde87e2ad43b5eb5104006214ac3
parentd4dbe64eb2ff8c040fe0bc89b33ec043565e5b6f (diff)
Makefile: slightly cleaner version of r10026
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10027 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.common4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index e42c83f0f7..0c37a3a7d4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -30,9 +30,9 @@ COQIDEOPT:=bin/coqide.opt$(EXE)
COQIDE:=bin/coqide$(EXE)
ifeq ($(BEST),opt)
-COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP)
+COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP)
else
-COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOP)
+COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOP)
endif
OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)