aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-05 17:58:39 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-05 17:58:39 +0200
commitcaacdb00c830854de72ba2fe19b5f74951d445bf (patch)
treea90fb194c2f00274fec0f3eeaba5ae30d6d0573c
parent3ded029b42c7acf0b1b575cf4f0bb395a1d0d823 (diff)
parent56001961201e3092005cd898151c8ba4b798b6ed (diff)
Merge PR #7991: Make Travis faster by removing more builds.
-rw-r--r--.travis.yml9
1 files changed, 0 insertions, 9 deletions
diff --git a/.travis.yml b/.travis.yml
index 627334690..42c41249d 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -67,9 +67,6 @@ matrix:
- TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-bignums"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-color"
- if: NOT (type = pull_request)
env:
@@ -85,9 +82,6 @@ matrix:
- TEST_TARGET="ci-equations"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-fcsl-pcm"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-fiat-parsers"
- if: NOT (type = pull_request)
env:
@@ -100,9 +94,6 @@ matrix:
- TEST_TARGET="ci-ltac2"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-math-classes"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-mtac2"
- if: NOT (type = pull_request)
env: