diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 13:30:26 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-26 13:30:26 -0700 |
commit | bf300b47de94182145f5c4d0f0ec0e7cf09b6143 (patch) | |
tree | 0e2baed73dde7aecb7c886641132465c216d983f /.travis.yml | |
parent | d0ce9d1dd563e6ec5c84743ced1b07ff0b3b9cb5 (diff) |
Regression level 0 for distcheck on Travis (#1714)
We are running all our Travis tests with regression level 0 except for
distcheck, which is running with the default level 1. This commit lowers
the level to 0 to make all jobs consistent.
Diffstat (limited to '.travis.yml')
-rw-r--r-- | .travis.yml | 2 |
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() { |