commit | 6741fc914851de968c9dfa5a690d1183b650b144 | [log] [tgz] |
---|---|---|
author | Dave Rodgman <dave.rodgman@arm.com> | Wed Apr 07 16:07:50 2021 +0100 |
committer | GitHub <noreply@github.com> | Wed Apr 07 16:07:50 2021 +0100 |
tree | 78f8bc5fab9af642e9356f84058d3ff5a571c484 | |
parent | 0708974d85df2b7a1a5229627ce8532bd8c07dc8 [diff] | |
parent | add60da95b7b8fe9c2ece6b10ab7cacebd95f7e1 [diff] |
Merge pull request #4306 from daverodgman/fix_mps_trace_macros Capitalise MPS trace macros
diff --git a/tests/scripts/check-names.sh b/tests/scripts/check-names.sh index 55f76da..293afa8 100755 --- a/tests/scripts/check-names.sh +++ b/tests/scripts/check-names.sh
@@ -28,11 +28,6 @@ exit fi -if grep --version|head -n1|grep GNU >/dev/null; then :; else - echo "This script requires GNU grep.">&2 - exit 1 -fi - trace= if [ $# -ne 0 ] && [ "$1" = "-v" ]; then shift