From 0ee40cbbf7df4c25a89920c4781c0bf23728c0cd Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Sun, 25 Aug 2019 10:31:38 +0200 Subject: Changed chmod -w to chmod a-w to avoid error on cygwin --- Makefile.ide | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.ide') diff --git a/Makefile.ide b/Makefile.ide index cb026cdf43..0a11f83a18 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -121,7 +121,7 @@ $(COQIDEBYTE): $(LINKIDE) ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile @rm -f $@ cp $< $@ - @chmod -w $@ + @chmod a-w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' -- cgit v1.2.3