From ddf7b82220a504a8af3ac6d2dfc9664300a1db82 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 20 Sep 2017 11:51:17 +0200 Subject: coq_makefile: dont show errors from failed (ignored) rmdir --- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 56e12a1e0..afe8e62ee 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -500,7 +500,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ done .PHONY: uninstall -- cgit v1.2.3