From: Brian Norris <banorris@uci.edu>
Date: Sat, 3 Nov 2012 02:37:20 +0000 (-0700)
Subject: bench: send timings to stdout, not stderr
X-Git-Tag: pldi2013~18
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=b4b1d528f7d1db77448a389776ecd5c95da2084a

bench: send timings to stdout, not stderr
---

diff --git a/bench.sh b/bench.sh
index a42fee7..8337ab3 100755
--- a/bench.sh
+++ b/bench.sh
@@ -37,7 +37,7 @@ function run_test {
 	echo "*******************************"
 	echo "Re-running test for timing data"
 	echo "*******************************"
-	time ${RUN} ${t} ${ARGS} > /dev/null 2>&1
+	(time ${RUN} ${t} ${ARGS} > /dev/null 2>&1) 2>&1
 	echo
 	echo "Test done; sleeping for a few seconds"
 	echo