Heed --quiet when running make generated_files

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>
2021-07-08 19:07:07 +02:00 · 2021-07-08 19:07:07 +02:00 · 7238503642
commit 7238503642
parent 88a07457c7
1 changed files with 5 additions and 1 deletions
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@ -713,7 +713,11 @@ pre_generate_files() {
    # since make doesn't have proper dependencies, remove any possibly outdate
    # file that might be around before generating fresh ones
    make neat
-    make generated_files
+    if [ $QUIET -eq 1 ]; then
+        make -s generated_files
+    else
+        make generated_files
+    fi
 }