commit 72385036420e9a072c0588ccd685f8f72cf6458d
author Gilles Peskine <Gilles.Peskine@arm.com> Thu Jul 08 19:07:07 2021 +0200
committer Gilles Peskine <Gilles.Peskine@arm.com> Mon Jul 12 18:19:31 2021 +0200
tree 4276e49ab6f56fcb134a92e9d94212c872eb13f0
parent 88a07457c7e6dbe0c170a75110f84bad39f156c6

Heed --quiet when running make generated_files

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>

tests/scripts/all.sh

diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index 4614029..c3df05b 100755
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@@ -713,7 +713,11 @@
     # 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
 }