diff options
| author | Jesusalva Jesusalva <jesusalva@themanaworld.org> | 2024-02-08 23:45:52 +0000 |
|---|---|---|
| committer | Administrator <admin@themanaworld.org> | 2024-02-08 23:45:52 +0000 |
| commit | 12a287e0aa7901fb412e5b0a8c5a77c9d236eda9 (patch) | |
| tree | 198d8c462c24fcc6cdbad4d77c2507739db862f8 /tools | |
| parent | 7a0c3cbf9143aaa9293c1048b15dc1cd63c2ce36 (diff) | |
| download | mv-12a287e0aa7901fb412e5b0a8c5a77c9d236eda9.tar.gz mv-12a287e0aa7901fb412e5b0a8c5a77c9d236eda9.tar.bz2 mv-12a287e0aa7901fb412e5b0a8c5a77c9d236eda9.tar.xz mv-12a287e0aa7901fb412e5b0a8c5a77c9d236eda9.zip | |
Be slightly more smart when running mplint
Reduce some overhead on the script for a 4% speedup
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/jobs/mplint.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/ci/jobs/mplint.sh b/tools/ci/jobs/mplint.sh index d3508759f..573cd1c85 100755 --- a/tools/ci/jobs/mplint.sh +++ b/tools/ci/jobs/mplint.sh @@ -25,7 +25,9 @@ run_configure_simple run_make cd .. echo " " >config.h -run_mplint $* +for task in "$@"; do + run_mplint $task +done source ./tools/ci/scripts/exit.sh |