Commit 5121f5e0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve indentation of bench output.

parent 4dfefc95
...@@ -87,7 +87,7 @@ invalid_goals () { ...@@ -87,7 +87,7 @@ invalid_goals () {
execute () { execute () {
pgm="bin/why3execute$suffix" pgm="bin/why3execute$suffix"
echo -n "$1 $2... " echo -n " $1 $2... "
if $pgm $1 $2 > /dev/null 2>&1; then if $pgm $1 $2 > /dev/null 2>&1; then
echo "ok" echo "ok"
else else
...@@ -103,7 +103,7 @@ extract_and_run () { ...@@ -103,7 +103,7 @@ extract_and_run () {
shift shift
prg=$1 prg=$1
shift shift
echo -n "$dir... " echo -n " $dir... "
rm -f $dir/$prg rm -f $dir/$prg
echo -n "clean... " echo -n "clean... "
if BENCH=yes make -C $dir clean > /dev/null 2>&1; then if BENCH=yes make -C $dir clean > /dev/null 2>&1; then
...@@ -150,7 +150,7 @@ extract_and_run () { ...@@ -150,7 +150,7 @@ extract_and_run () {
list_stuff () { list_stuff () {
pgm="bin/why3$suffix" pgm="bin/why3$suffix"
echo -n "$1 " echo -n " $1 "
if $pgm $1 > /dev/null 2>&1; then if $pgm $1 > /dev/null 2>&1; then
echo "ok" echo "ok"
else else
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment