Add timing to script

tbidne · Nov 7, 2024 · 9507e2d · 9507e2d
1 parent b063766
commit 9507e2d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/run_tools.sh b/test/run_tools.sh
@@ -39,7 +39,7 @@ any_failed=0
 for tool in $tools; do
   echo "*** TESTING: $tool ***"
 
-  run_tool $tool
+  time run_tool $tool
 
   exit_code=$?
   if [[ $exit_code -ne 0 ]]; then