From d4dbe64eb2ff8c040fe0bc89b33ec043565e5b6f Mon Sep 17 00:00:00 2001
From: lmamane
Date: Wed, 18 Jul 2007 16:01:32 +0000
Subject: Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte,
 it complains.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10026 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Makefile.common b/Makefile.common
index 41603fef6b..e42c83f0f7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,7 +29,11 @@ COQIDEBYTE:=bin/coqide.byte$(EXE)
 COQIDEOPT:=bin/coqide.opt$(EXE)
 COQIDE:=bin/coqide$(EXE)
 
+ifeq ($(BEST),opt)
 COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP)
+else
+COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE)               $(COQTOP)
+endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
 MINICOQ:=bin/minicoq$(EXE)
-- 
cgit v1.2.3