Fix benchmarking for failing tests

GaloisInc · Aug 28, 2024 · f7aa970 · f7aa970
1 parent aaf8354
commit f7aa970
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.