From 4076472844485e077ea612140e4a5f9d72d15181 Mon Sep 17 00:00:00 2001
From: Alexander Boettcher <alexander.boettcher@genode-labs.com>
Date: Tue, 4 Oct 2016 12:00:18 +0200
Subject: [PATCH] tool: kill all children of rump tool

Issue #2110
---
 tool/rump | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tool/rump b/tool/rump
index 2166a0d18..3364ff8a4 100755
--- a/tool/rump
+++ b/tool/rump
@@ -32,6 +32,7 @@ trap_exit() {
 	fi
 
 	[ -d "$RUMP_TMP" ] && rm -rf $RUMP_TMP
+	pkill -P $$
 }