From dc30332cf167feafe7b123e2b75d57e03a68e50d Mon Sep 17 00:00:00 2001
From: Jesusaves <cpntb1@ymail.com>
Date: Sun, 25 Jun 2023 16:47:29 -0300
Subject: Be slightly more smart when running mplint

Inspired by https://stackoverflow.com/questions/918886/how-do-i-split-a-string-on-a-delimiter-in-bash
why tf were we recompiling mplint three times, anyway.
---
 tools/ci/jobs/mplint.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/ci/jobs/mplint.sh b/tools/ci/jobs/mplint.sh
index d3508759f..c1e817479 100755
--- a/tools/ci/jobs/mplint.sh
+++ b/tools/ci/jobs/mplint.sh
@@ -25,7 +25,11 @@ run_configure_simple
 run_make
 cd ..
 echo " " >config.h
-run_mplint $*
+tasks=$(echo $* | tr " " "\n")
+for task in $tasks
+do
+    run_mplint $task
+done
 
 source ./tools/ci/scripts/exit.sh
 
-- 
cgit v1.2.3-60-g2f50