aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/.csdp.cachebin89077 -> 89077 bytes
-rw-r--r--tools/CoqMakefile.in5
2 files changed, 2 insertions, 3 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd..b99d80e95 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fb064c495..1308e9175 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -375,7 +375,7 @@ uninstall::
instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \
rm -f "$$instf";\
echo RM "$$instf"; \
- rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \
+ rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \
done
.PHONY: uninstall
@@ -385,8 +385,7 @@ uninstall-doc::
$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
- $(HIDE)rmdir --ignore-fail-on-non-empty \
- "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/"
+ $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
.PHONY: uninstall-doc
# Cleaning ####################################################################