From 8a96d44ed475890d722f98166c864b820e2e5d86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?H=C3=A9ctor=20Molinero=20Fern=C3=A1ndez?= Date: Sun, 2 Jun 2019 10:42:23 +0200 Subject: [PATCH] Do not delete "dist" directory if it is not empty --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 0b90164..6f7b3fb 100644 --- a/Makefile +++ b/Makefile @@ -108,4 +108,4 @@ version: .PHONY: clean clean: rm -f '$(IMAGE_TARBALL)' - if [ -d '$(DISTDIR)' ]; then rmdir '$(DISTDIR)'; fi + if [ -d '$(DISTDIR)' ] && [ -z "$$(ls -A '$(DISTDIR)')" ]; then rmdir '$(DISTDIR)'; fi