aboutsummaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml2
1 files changed, 2 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
index 7138d5c61e..81f50af0a0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -40,6 +40,7 @@ env:
- TEST_TARGET="ci-math-comp"
- TEST_TARGET="ci-sf"
- TEST_TARGET="ci-unimath"
+ - TEST_TARGET="ci-vst"
# Not ready yet for 8.7
# - TEST_TARGET="ci-cpdt"
# - TEST_TARGET="ci-metacoq"
@@ -49,6 +50,7 @@ matrix:
allow_failures:
- env: TEST_TARGET="ci-geocoq"
+ - env: TEST_TARGET="ci-vst"
# Full Coq test-suite with two compilers
# [TODO: use yaml refs and avoid duplication for packages list]