tool: kill all children of rump tool

Issue #2110
2016-10-04 12:00:18 +02:00 · 2016-10-04 12:00:18 +02:00 · 4076472844
parent a0c9915cee
commit 4076472844
1 changed files with 1 additions and 0 deletions
--- a/tool/rump
+++ b/tool/rump
@ -32,6 +32,7 @@ trap_exit() {
 	fi

 	[ -d "$RUMP_TMP" ] && rm -rf $RUMP_TMP
+	pkill -P $$
 }