From f1185813cac9aacefdb050266005c1c6aa22fe67 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pedro=20Gon=C3=A7alves?= <pedro@lsts.pt>
Date: Wed, 12 Dec 2018 14:37:05 +0000
Subject: [PATCH] docker: fix option to delete docker img.

---
 docker/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docker/Makefile b/docker/Makefile
index 98a1dd8..6aa1b0f 100644
--- a/docker/Makefile
+++ b/docker/Makefile
@@ -40,4 +40,4 @@ clean:
 	@echo "* Done."
 
 delete_img:
-    sudo docker system prune -a
+	@sudo docker system prune -a