diff options
| -rwxr-xr-x | tools/run-test-valgrind.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/run-test-valgrind.sh b/tools/run-test-valgrind.sh index 7eac4a80b7..fb8cb1482e 100755 --- a/tools/run-test-valgrind.sh +++ b/tools/run-test-valgrind.sh @@ -27,6 +27,11 @@ $LIBTOOL --mode=execute "$VALGRIND" \ "$TEST" RESULT=$? +if [ $RESULT -eq 0 -a "$(wc -c "$LOGFILE" | awk '{print$1}')" -ne 0 ]; then + echo "valgrind succeeded, but log is not empty: $LOGFILE" + exit 1 +fi + if [ $RESULT -ne 0 -a $RESULT -ne 77 ]; then echo "Don't forget to check the valgrind log at '`realpath $LOGFILE`'." >&2 fi |