From 9f9012667e7b1b0caea15ae39555e9d6bdbd00e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20Papou=C5=A1ek?= <jan.papousek@gmail.com>
Date: Wed, 1 May 2013 23:24:43 +0200
Subject: [PATCH] fixed script for shutting down servers

---
 benchmark/bench.sh  | 4 +++-
 servers-shutdown.sh | 5 +++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/benchmark/bench.sh b/benchmark/bench.sh
index 1345f759..5b2c3eb4 100755
--- a/benchmark/bench.sh
+++ b/benchmark/bench.sh
@@ -2,6 +2,7 @@
 SELF=`readlink -f $0`
 SELF_DIR=`dirname $SELF`
 BENCHMARK_LIST_FILE=$1
+set -x
 
 if [ -z $BASH_EXEC ]; then
 	BASH_EXEC=/bin/sh
@@ -56,6 +57,7 @@ for LINE in `cat $BENCHMARK_LIST_FILE`; do
 
 	if [[ $CONFIG =~ .*dist.* ]]; then
 		echo "## stopping servers";
-		$BASH_EXEC $SELF_DIR/../servers-shutdown.sh $SELF_DIR/configs/$CONFIG.xml;
+		COMMAND="$BASH_EXEC $SELF_DIR/../servers-shutdown.sh $SELF_DIR/configs/$CONFIG.xml";
+		eval $COMMAND;
 	fi
 done
diff --git a/servers-shutdown.sh b/servers-shutdown.sh
index eb822bc5..dbe64809 100755
--- a/servers-shutdown.sh
+++ b/servers-shutdown.sh
@@ -2,6 +2,7 @@
 SELF=`readlink -f $0`
 SELF_DIR=`dirname $SELF`
 CONFIG_FILE=$1
+set -x;
 
 usage()
 {
@@ -21,9 +22,9 @@ if [ "$CONFIG_FILE" == "" ]; then
 fi
 
 for IP in `grep "<value>" $CONFIG_FILE | tr '<>' ' ' | awk '{ print $2 }'`; do
-	PROCESSES=`ssh $IP -t "ps -ux | grep parasim" | awk '{print $2}'`
+	PROCESSES=`ssh $IP "ps -ux | grep parasim" | awk '{print $2}'`;
 	for PROCESS in $PROCESSES; do
-		ssh $IP -t "kill -9 $PROCESS"
+		ssh $IP "kill -9 $PROCESS";
 	done
 	echo "server $IP killed";
 done