From d9952dc6cf0ffdd5ffade499d6eff79ff3e51c1e Mon Sep 17 00:00:00 2001 From: Sebastian Date: Fri, 2 Feb 2018 11:27:38 +0100 Subject: [PATCH] tools/run_more_tests.sh: Fixed comment Name of the script that uses this script was wrong. --- tools/run_more_tests.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/run_more_tests.sh b/tools/run_more_tests.sh index 27cd989a8..4072635de 100755 --- a/tools/run_more_tests.sh +++ b/tools/run_more_tests.sh @@ -1,5 +1,5 @@ #!/bin/bash -# Script Used by generate_and_run_tests.sh +# Script Used by generate_and_run_more_tests.sh set -e