echo
echo "...from the 'tests' directory. Note that subsequent calls to "
echo "run_tests.sh with --coverage will klobber previous results. See:"
echo
echo "...from the 'tests' directory. Note that subsequent calls to "
echo "run_tests.sh with --coverage will klobber previous results. See:"