aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-24 16:32:44 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-10-25 13:42:41 +0200
commit7bd0fc03e5656e6672e8329b070ca9bda88d6b99 (patch)
treee83c3bd620cf41a43d46587f2ddc4fba630590df /.travis.yml
parentd3de8fe500c736aa92aa87c9cd8b83fa4f44b7d8 (diff)
Put linter at the top of the tests.
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml22
1 files changed, 11 insertions, 11 deletions
diff --git a/.travis.yml b/.travis.yml
index c99a3db4e..22ae6b7aa 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -64,6 +64,17 @@ env:
matrix:
include:
+ - env:
+ - TEST_TARGET="lint"
+ install: []
+ before_script: []
+ addons:
+ apt:
+ sources: []
+ packages: []
+ script:
+ - dev/lint-repository.sh
+
# Full Coq test-suite with two compilers
- env:
- TEST_TARGET="test-suite"
@@ -135,17 +146,6 @@ matrix:
- avsm
packages: *coqide-packages
- - env:
- - TEST_TARGET="lint"
- install: []
- before_script: []
- addons:
- apt:
- sources: []
- packages: []
- script:
- - dev/lint-repository.sh
-
- os: osx
osx_image: xcode8.3
env: