aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
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.build
parent74640d2b8bc158b301c0646db19747a86313e25a (diff)
Rebuild coqtop$(EXE) in "make coqbinaries" in addition to coqtop.opt$(EXE).
Fixes #7758.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index ed251af77..60682c6e3 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -387,12 +387,12 @@ grammar/%.cmi: grammar/%.mli
.PHONY: coqbinaries coqbyte
-coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
coqbyte: $(TOPBYTE) $(CHICKENBYTE)
# Special rule for coqtop, we imitate `ocamlopt` can delete the target
# to avoid #7666
-$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
+$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
rm -f $@ && cp $< $@
bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)