From a5d6cbf44d6c47d75eca4838dd576fd3c0568ea0 Mon Sep 17 00:00:00 2001
From: Christian Prochaska <christian.prochaska@genode-labs.com>
Date: Tue, 21 May 2019 13:19:59 +0200
Subject: [PATCH] tool_chain: strip gdb

Issue #3307
---
 tool/tool_chain | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tool/tool_chain b/tool/tool_chain
index 22b6801cd0..cb6aada9ff 100755
--- a/tool/tool_chain
+++ b/tool/tool_chain
@@ -508,6 +508,7 @@ $(GDB_BINARIES): $(BUILD_LOCATION)/$(PLATFORM)/gdb/Makefile
 $(GDB_INSTALLED_BINARIES): $(GDB_BINARIES)
 	$(ECHO) "$(BRIGHT_COL)installing gdb...$(DEFAULT_COL)"
 	$(VERBOSE)$(MAKE) -C $(BUILD_LOCATION)/$(PLATFORM)/gdb install $(MAKE_OPT) MAKEINFO=true
+	$(VEBOSE)strip $@
 
 $(BUILD_LOCATION)/ali2dep/build/build.gpr:
 	$(ECHO) "$(BRIGHT_COL)preparing ali2dep...$(DEFAULT_COL)"