summaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-03-26 21:03:31 -0500
committerGitHub <noreply@github.com>2018-03-26 21:03:31 -0500
commit931c3153bcf62e2768bc80fa17a4280ab67ff2d0 (patch)
tree74a8c90517ec1711dcc4faa65c0620ffe298b9de /.travis.yml
parentc80d9a4708c989dd4e753acce662a70eaa633a1c (diff)
parentab70f7a01939515792221b33372ec994bd425fde (diff)
Merge branch 'master' into rewrite_concatrewrite_concat
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml
index 94cee00ab..d1f72f955 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -77,7 +77,7 @@ script:
exit 1;
}
makeDistcheck() {
- make V=1 -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' ||
+ make V=1 -j2 distcheck REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' ||
error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
}
makeCheck() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback