Make --quiet more effective when running make generated_files

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>
diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index 2dc1375..7e8b2c3 100755
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@@ -752,7 +752,7 @@
     # 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