diff --git a/test/run_tools.sh b/test/run_tools.sh index ffd0185..5b1721c 100755 --- 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