From 7530163f3b003e4851a48cb5661b1b1d4dbf6e6a Mon Sep 17 00:00:00 2001
From: Gilles Peskine <Gilles.Peskine@arm.com>
Date: Thu, 5 Aug 2021 15:10:47 +0200
Subject: [PATCH] Make --quiet more effective when running make generated_files

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

diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index 2dc13756a..7e8b2c3c2 100755
--- 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