From b0623a2803acb1c59b1bde10343ca9826f67b759 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Hoguin?= <essen@ninenines.eu>
Date: Fri, 15 Sep 2017 22:21:47 +0200
Subject: Fix removal of COVER_DATA_DIR if not empty

---
 plugins/cover.mk | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/cover.mk')

diff --git a/plugins/cover.mk b/plugins/cover.mk
index b57458a..a14b992 100644
--- a/plugins/cover.mk
+++ b/plugins/cover.mk
@@ -80,7 +80,9 @@ ifneq ($(COVER_REPORT_DIR),)
 .PHONY: cover-report-clean cover-report
 
 cover-report-clean:
-	$(gen_verbose) rm -rf $(COVER_REPORT_DIR) $(COVER_DATA_DIR)
+	$(gen_verbose) rm -rf $(COVER_REPORT_DIR)
+	# Remove the COVER_DATA_DIR only if it is empty.
+	-$(verbose) rmdir $(COVER_DATA_DIR)
 
 ifeq ($(COVERDATA),)
 cover-report:
-- 
cgit v1.2.3