summaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
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