From 16897f70147a95e3a21e322d7b58b8dd0fa0891f Mon Sep 17 00:00:00 2001
From: Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de>
Date: Fri, 21 Aug 2015 03:09:10 +0200
Subject: [PATCH] Linux Makefile: Remove EXECUTABLE_STRIPPED file on clean

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

diff --git a/shell/linux/Makefile b/shell/linux/Makefile
index 60fed85f2..1870ef2f1 100644
--- a/shell/linux/Makefile
+++ b/shell/linux/Makefile
@@ -275,4 +275,4 @@ obj-$(platform)/%.build_obj : $(RZDCY_SRC_DIR)/%.S
 	$(AS) $(ASFLAGS) $(INCS) $< -o $@
 
 clean:
-	rm -f $(OBJECTS) $(EXECUTABLE) .map
+	rm -f $(OBJECTS) $(EXECUTABLE) $(EXECUTABLE_STRIPPED) .map