From f7aa970e984e21d14cabed58397750ca4c317755 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 27 Aug 2024 14:18:55 -0400
Subject: [PATCH] Fix benchmarking for failing tests

---
 tests/run-ci-benchmarks.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 6230713c3..f209dfd05 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -19,7 +19,7 @@ INDEX=0
 for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
-  /usr/bin/time -f "%e" -o /tmp/time cn verify "${TEST}" || true
+  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${TEST}" || true
   TIME=$(cat /tmp/time)
 
   # If we're last, don't print a trailing comma.