From 72385036420e9a072c0588ccd685f8f72cf6458d Mon Sep 17 00:00:00 2001
From: Gilles Peskine <Gilles.Peskine@arm.com>
Date: Thu, 8 Jul 2021 19:07:07 +0200
Subject: [PATCH] Heed --quiet when running make generated_files

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>
---
 tests/scripts/all.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index 4614029ad0..c3df05b724 100755
--- 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
 }