aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-10-22 10:46:14 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2017-11-20 10:22:17 +0100
commit9826bbd4eb1ded394d38a94abff25baa71823221 (patch)
tree8e2ae9636fbc3d48a3921c3ee9eb9445de450f3d /.travis.yml
parentedf1a8f36f75861b822081b3825357e122b6937d (diff)
Add Equations to CI
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
index 3ebfbefd2..1f6bb11e0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -50,6 +50,7 @@ env:
- TEST_TARGET="ci-compcert TIMED=1"
- TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
- TEST_TARGET="ci-coquelicot TIMED=1"
+ - TEST_TARGET="ci-equations TIMED=1"
- TEST_TARGET="ci-geocoq TIMED=1"
- TEST_TARGET="ci-fiat-crypto TIMED=1"
- TEST_TARGET="ci-fiat-parsers TIMED=1"