[CI] run-pylint: Use pylint if pylint3 is missing

Starting from Ubuntu 19.10 pylint3 was replaced with pylint.
This commit is contained in:
Isaku Yamahata
2020-01-23 22:20:54 +01:00
committed by Michał Kowalczyk
parent 2ddd53b102
commit f5974b027d
+7 -1
View File
@@ -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