diff options
Diffstat (limited to 'tools/ci/jobs')
-rwxr-xr-x | tools/ci/jobs/mplint.sh | 25 |
1 files changed, 7 insertions, 18 deletions
diff --git a/tools/ci/jobs/mplint.sh b/tools/ci/jobs/mplint.sh index 573cd1c85..60422e5f6 100755 --- a/tools/ci/jobs/mplint.sh +++ b/tools/ci/jobs/mplint.sh @@ -1,29 +1,18 @@ #!/usr/bin/env bash -export CC=gcc -export CXX=g++ - -if [ "$NEWCC" != "" ]; then - export CC="$NEWCC" -fi -if [ "$NEWCXX" != "" ]; then - export CXX="$NEWCXX" -fi +set -e # Fail if any command fails +set -u # Fail if any variable is unset when used export LOGFILE=mplint_po.log - source ./tools/ci/scripts/init.sh -export CXXFLAGS="-std=gnu++11" +rm -rf mplint || true +tools/ci/scripts/retry.sh wget -O mplint-release.zip "$MPLINT_PACKAGE_URL" +unzip mplint-release.zip -do_init +read mplint_commit < mplint-version.txt +printf "Using mplint: %s\n" "$mplint_commit" -rm -rf mplint || true -gitclone https://git.themanaworld.org/mana mplint.git -cd mplint -run_configure_simple -run_make -cd .. echo " " >config.h for task in "$@"; do run_mplint $task |