diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 94b965a7f..bb6302a98 100644 --- a/Makefile.common +++ b/Makefile.common @@ -14,8 +14,8 @@ # Executables ########################################################################### -TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker)) -TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE)) +TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker)) +TOPBYTE:=$(TOPBINOPT:.opt$(EXE)=.byte$(EXE)) COQTOPEXE:=bin/coqtop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) |