From cc7e298cf9d19f6f7230a4796b945836c30f1ccd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 10:03:16 +0000 Subject: [PATCH] Nicer output for the "make tests*" commands. --- helm/matita/scripts/do_tests.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh index 080ff2ada..d2e7eec91 100755 --- a/helm/matita/scripts/do_tests.sh +++ b/helm/matita/scripts/do_tests.sh @@ -36,15 +36,15 @@ fi TMP=.__temp.txt for T in $TODO; do - echo -en "$COMPILER\t$T\t" + printf "$COMPILER\t%-30s " $T if [ "$TWICE" = "1" ]; then $COMPILER $T 1>/dev/null 2>/dev/null fi - /usr/bin/time --quiet -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1 + /usr/bin/time --quiet -o $TMP -f "%E %U %S" $COMPILER $T >> $LOGFILE 2>&1 if [ $? = 0 ]; then - echo -e "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA" + printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n" else - echo -e "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA" + printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n" fi done -- 2.39.2