diff --git a/util/lint/lint b/util/lint/lint index 826685d292..772d8bdaeb 100755 --- a/util/lint/lint +++ b/util/lint/lint @@ -50,15 +50,14 @@ for script in "$(dirname "$0")/${1}-"*; do grep "^# DESCR:" "$script" | sed "s,.*DESCR: *,," echo "========" junit_write " " - $script > "$LINTLOG" + $script | tee "$LINTLOG" #if the lint script gives any output, that's a failure if [ "$(wc -l < "$LINTLOG")" -eq 0 ]; then echo "success" junit_write " " else - echo "test failed:" - cat "$LINTLOG" + echo "test failed" junit_write " "