diff options
| -rw-r--r-- | Makefile.common | 4 |
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) |