From 305c8dc1a8518388077c5f2d063f793a2c2e39da Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 1 Jun 2017 15:41:36 +0200
Subject: Fix coq_makefile uninstall target under OSX.

---
 tools/CoqMakefile.in | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fb064c495f..1308e91759 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 ####################################################################
-- 
cgit v1.2.3