diff options
Diffstat (limited to '.ci/script.sh')
| -rwxr-xr-x | .ci/script.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.ci/script.sh b/.ci/script.sh index 4d0666ec0e..c3c7b8dfa9 100755 --- a/.ci/script.sh +++ b/.ci/script.sh @@ -4,7 +4,7 @@ set -e set -o pipefail if [[ -n "${CI_TARGET}" ]]; then - make lint + make "${CI_TARGET}" exit 0 fi |