summaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-02-16 07:05:14 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-02-16 09:05:14 -0600
commitae2fb8ac9f22c9ad65a3d08dfe8319ea0160b0ea (patch)
treeb4a2af8d465e955976909348f0acf2f6d15735c7 /.travis.yml
parent81f8a73120f3237baabad1faa2c467d1759d56d7 (diff)
Make regress1 default, only test regress0 on Travis. (#1611)
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml4
1 files changed, 3 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml
index 562987f3c..e8c858d18 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -81,7 +81,9 @@ script:
error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
}
makeCheck() {
- make V=1 -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
+ make V=1 -j2 units || error "BUILD/UNIT TEST FAILED";
+ make V=1 -j2 systemtests || error "BUILD/SYSTEM TEST FAILED";
+ make V=1 -j2 regress0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/REGRESSION TEST FAILED";
}
makeExamples() {
make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback