diff options
| author | Jesusaves <cpntb1@ymail.com> | 2023-06-25 16:47:29 -0300 |
|---|---|---|
| committer | Jesusaves <cpntb1@ymail.com> | 2023-06-25 16:47:29 -0300 |
| commit | dc30332cf167feafe7b123e2b75d57e03a68e50d (patch) | |
| tree | ceff8f79eeed205cdaa0ef8bf3ac407f57ddd2aa /tools/ci/jobs | |
| parent | c5bc7240438be03fd0181be39a635cc06557324f (diff) | |
| download | plus-jesusalva/mplint.tar.gz plus-jesusalva/mplint.tar.bz2 plus-jesusalva/mplint.tar.xz plus-jesusalva/mplint.zip | |
Be slightly more smart when running mplintjesusalva/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.
Diffstat (limited to 'tools/ci/jobs')
| -rwxr-xr-x | tools/ci/jobs/mplint.sh | 6 |
1 files changed, 5 insertions, 1 deletions
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 |