diff options
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 4 insertions, 0 deletions
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) |