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 indentation detected" + echo "ERROR: mixed indentation detected" st=1 fi; nl='