Make --quiet more effective when running make generated_files

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>
2021-08-05 15:10:47 +02:00 · 2021-08-05 15:10:47 +02:00 · 7530163f3b
commit 7530163f3b
parent 3cbd69c4d4
1 changed files with 1 additions and 1 deletions
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@ -752,7 +752,7 @@ pre_generate_files() {
    # file that might be around before generating fresh ones
    make neat
    if [ $QUIET -eq 1 ]; then
-        make -s generated_files
+        make generated_files >/dev/null
    else
        make generated_files
    fi