summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-08-01 13:04:07 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2018-08-01 13:04:07 -0700
commit7e1b64d6ef8444b003545fdeca90304ac3d46621 (patch)
tree5fbb841f218123083a4d976b7ebaf0dacab9f203
parent2b849f3f9357685a5ac5d9cd2615a77435ded013 (diff)
-rw-r--r--.travis.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml
index a7c583dff..218d14df9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -81,8 +81,8 @@ script:
error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
}
makeCheck() {
- builds/bin/cvc4 --show-config
make V=1 -j2 check REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED"
+ builds/bin/cvc4 --show-config
}
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