From ed642a9311e3cb9d63ca2a202dd9375519e6ff2f Mon Sep 17 00:00:00 2001
From: oranges <email@oranges.net.nz>
Date: Wed, 13 Jul 2022 15:34:45 +1200
Subject: [PATCH] The lint for whitespace issues now shouts louder (#68386)

---
 tools/ci/check_grep.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/ci/check_grep.sh b/tools/ci/check_grep.sh
index 55d81b57061..6ac8b36c1de 100755
--- a/tools/ci/check_grep.sh
+++ b/tools/ci/check_grep.sh
@@ -168,11 +168,11 @@ if grep -P '^/*var/' code/**/*.dm; then
 fi;
 echo "Checking for whitespace issues"
 if grep -P '(^ {2})|(^ [^ * ])|(^    +)' code/**/*.dm; then
-    echo "space indentation detected"
+    echo "ERROR: space indentation detected"
     st=1
 fi;
 if grep -P '^\t+ [^ *]' code/**/*.dm; then
-    echo "mixed <tab><space> indentation detected"
+    echo "ERROR: mixed <tab><space> indentation detected"
     st=1
 fi;
 nl='