diff --git a/doc/lua/test_single.sh b/doc/lua/test_single.sh index aa0261e4e0..67de6ab5be 100755 --- a/doc/lua/test_single.sh +++ b/doc/lua/test_single.sh @@ -13,6 +13,7 @@ if $LEANLUA $f.lua > $f.produced.out; then echo "-- worked" exit 0 else - echo "ERROR executing $f.lua, produced output is at $f.produced.out" + echo "ERROR executing $f.lua, produced output:" + cat $f.produced.out exit 1 fi diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index 21b0fb4a5e..a2fea543f8 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -24,6 +24,8 @@ if test -f $f.expected.out; then if diff $f.produced.out $f.expected.out; then echo "-- mismath was fixed" fi + else + diff $f.produced.out $f.expected.out fi exit 1 fi diff --git a/tests/lua/test_single.sh b/tests/lua/test_single.sh index fe46e3ae7d..ba05e3e031 100755 --- a/tests/lua/test_single.sh +++ b/tests/lua/test_single.sh @@ -11,6 +11,7 @@ if $LEANLUA util.lua $f > $f.produced.out; then echo "-- worked" exit 0 else - echo "ERROR executing $f, produced output is at $f.produced.out" + echo "ERROR executing $f, produced output:" + cat $f.produced.out exit 1 fi