diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-29 14:23:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-29 14:23:52 +0200 |
| commit | 26ca5d70f61f659b88a776c3253533dfbadccaee (patch) | |
| tree | 1eba87b7c91190f3d7bc2f31af7e000775f22d00 /Makefile.build | |
| parent | acbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff) | |
[build] Remove target binary before copy.
Fixes #7666. Due to shared mapping of executables Linux doesn't allow
to overwrite binaries that are running; we do as `ocamlopt` and delete
the target file before copy.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 5 |
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 $@' |