@@ -7,6 +7,9 @@
77# USE_GAUGE: whether to use gauge or tasty-bench
88# LONG: whether to use a large stream size
99
10+set -e
11+set -o pipefail
12+
1013# $1: message
1114die () {
1215 >&2 echo -e "Error: $1"
@@ -183,9 +186,9 @@ then
183186 # XXX this is a hack to make the "/" separated names used in the functions
184187 # determining options based on benchmark name. For tasty-bench the benchmark
185188 # names are separated by "." instead of "/".
186− BENCH_NAME=$(echo $BENCH_NAME_ORIG | sed -e s/^All\.//)
187− BENCH_NAME1=$(echo $BENCH_NAME | cut -f1 -d '/')
188− BENCH_NAME2=$(echo $BENCH_NAME | cut -f2- -d '/' | sed -e 's/\./\//g')
189+ BENCH_NAME0=$(echo $BENCH_NAME_ORIG | sed -e s/^All\.//)
190+ BENCH_NAME1=$(echo $BENCH_NAME0 | cut -f1 -d '/')
191+ BENCH_NAME2=$(echo $BENCH_NAME0 | cut -f2- -d '/' | sed -e 's/\./\//g')
189192 BENCH_NAME="$BENCH_NAME1/$BENCH_NAME2"
190193else
191194 BENCH_NAME=$BENCH_NAME_ORIG
@@ -219,7 +222,7 @@ then
219222 STREAM_SIZE_OPT="--stream-size $STREAM_SIZE"
220223fi
221224
222−echo "$BENCH_NAME: \
225+echo "$BENCH_NAME_ORIG: \
223226$RTS_OPTIONS \
224227$STREAM_LEN \
225228$QUICK_BENCH_OPTIONS" \