diff --git a/.ci/run-pylint b/.ci/run-pylint index b321ed60..1a7271d6 100755 --- a/.ci/run-pylint +++ b/.ci/run-pylint @@ -4,10 +4,16 @@ set -e cd "$(git rev-parse --show-toplevel)" +# pylint3 was replaced with pylint from Ubuntu 19.10 +PYLINT=$(command -v pylint3) +if [ -z "$PYLINT" ]; then + PYLINT=$(command -v pylint) +fi + find . -name \*.py \ -and -not -path ./LibOS/shim/test/apps/ltp/src/\* \ | sed 's/./\\&/g' \ -| xargs pylint3 "$@" \ +| xargs "${PYLINT}" "$@" \ Pal/src/host/Linux-SGX/signer/pal-sgx-get-token \ Pal/src/host/Linux-SGX/signer/pal-sgx-sign \ .ci/prfilter