diff options
| author | Gaëtan Gilbert | 2018-01-08 23:38:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-01-08 23:38:32 +0100 |
| commit | c671d86beecb4e31ad5c7752f7e4fb570823e837 (patch) | |
| tree | 198cfdd80f336c585fef35aa94ba60c0ab5b8b2c /dev | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Cleanup conditional in lint-repository.sh
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-repository.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 87a8297461..95b72787fb 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,7 +9,7 @@ CODE=0 -if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; +if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ]; then # skip PRs from before the linter existed if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; @@ -22,8 +22,8 @@ then # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} - MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD) - dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1 + MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD") + dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1 fi # Check that the files with 'whitespace' gitattribute end in a newline. |