diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-24 14:41:36 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-25 13:42:37 +0200 |
| commit | d3de8fe500c736aa92aa87c9cd8b83fa4f44b7d8 (patch) | |
| tree | d85956c39c66544d284da0d17ce70ab972c933c9 /.travis.yml | |
| parent | 4c954a3479e002d3a350c3094ae73e6ca5865202 (diff) | |
Linter: check that files end with newlines.
We use git check-attr to look at the same files as git diff --check.
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/.travis.yml b/.travis.yml index 4e937b50f..c99a3db4e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -135,8 +135,7 @@ matrix: - avsm packages: *coqide-packages - - if: type = pull_request - env: + - env: - TEST_TARGET="lint" install: [] before_script: [] @@ -145,10 +144,7 @@ matrix: sources: [] packages: [] script: - - 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 + - dev/lint-repository.sh - os: osx osx_image: xcode8.3 |