diff options
| -rwxr-xr-x | scripts/dev/pylint-ci.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/scripts/dev/pylint-ci.sh b/scripts/dev/pylint-ci.sh index 0ae2cfd9a..64cf45784 100755 --- a/scripts/dev/pylint-ci.sh +++ b/scripts/dev/pylint-ci.sh @@ -1,4 +1,8 @@ #!/bin/sh + +# exit when any command fails +set -e + PYLINT=${PYLINT:-pylint} "$PYLINT" --version |