aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-06-30 13:57:44 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-06-30 13:57:44 +0200
commit74640d2b8bc158b301c0646db19747a86313e25a (patch)
tree67be5b0d4c5bd334c8bd229b26de0adf4c5cb80d /Makefile.build
parent6055b1584b84c3ea5d8c1a4550e1eb0540d35421 (diff)
parent26ca5d70f61f659b88a776c3253533dfbadccaee (diff)
Merge PR #7960: [build] Remove target binary before copy.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index b85418243..ed251af77 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -390,9 +390,10 @@ grammar/%.cmi: grammar/%.mli
coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
coqbyte: $(TOPBYTE) $(CHICKENBYTE)
-# Special rule for coqtop
+# Special rule for coqtop, we imitate `ocamlopt` can delete the target
+# to avoid #7666
$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
- cp $< $@
+ rm -f $@ && cp $< $@
bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'