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