aboutsummaryrefslogtreecommitdiff
path: root/Makefile.ide
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.ide')
-rw-r--r--Makefile.ide8
1 files changed, 3 insertions, 5 deletions
diff --git a/Makefile.ide b/Makefile.ide
index 39c6c8ad1e..bd72494289 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -110,7 +110,7 @@ $(COQIDE): $(LINKIDEOPT)
$(STRIP_HIDE) $@
else
$(COQIDE): $(COQIDEBYTE)
- cp $< $@
+ rm -f $@ && cp $< $@
endif
$(COQIDEBYTE): $(LINKIDE)
@@ -119,9 +119,7 @@ $(COQIDEBYTE): $(LINKIDE)
-linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
- @rm -f $@
- cp $< $@
- @chmod a-w $@
+ rm -f $@ && cp $< $@ && chmod a-w $@
ide/%.cmi: ide/%.mli
$(SHOW)'OCAMLC $<'
@@ -150,7 +148,7 @@ IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa)
# Special rule for coqidetop
$(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
- cp $< $@
+ rm -f $@ && cp $< $@
$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
$(SHOW)'COQMKTOP -o $@'