1 files changed, 7 insertions, 5 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh
index 4b0764488..656a4d765 100755
--- a/tools/ci/scripts/init.sh
+++ b/tools/ci/scripts/init.sh
@@ -242,10 +242,12 @@ function run_tarball {
 function run_mplint {
     rm $ERRFILE
     echo "mplint/src/mplint $*"
-    mplint/src/mplint $* \
-    | grep -v "src/unittests/doctest.h" \
-    | grep -v "src/unittests/catch.hpp" \
-    | grep -v "src/debug/" \
-    >$ERRFILE
+    mplint/src/mplint "$@" \
+      | grep -v \
+             -e "src/unittests/doctest.h" \
+             -e "src/unittests/catch.hpp" \
+             -e "src/debug/" \
+        > "$ERRFILE"
+
     run_check_warnings
 }