aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.install
diff options
context:
space:
mode:
authorGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-06-28 13:04:27 -0700
committerGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-06-30 10:21:21 -0700
commit069d17f4f138fd779eff589119a7783784ababd9 (patch)
tree0a7fb0841703b7273f4609f3a0744e452239b78b /Makefile.install
parent74640d2b8bc158b301c0646db19747a86313e25a (diff)
Rebuild coqtop$(EXE) in "make coqbinaries" in addition to coqtop.opt$(EXE).
Fixes #7758.
Diffstat (limited to 'Makefile.install')
-rw-r--r--Makefile.install2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.install b/Makefile.install
index 010e35d42..21015d336 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -70,7 +70,7 @@ endif
install-binaries: install-tools
$(MKDIR) $(FULLBINDIR)
- $(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
+ $(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
install-byte: install-coqide-byte
$(MKDIR) $(FULLBINDIR)