summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-10-20 06:47:48 -0700
committerGitHub <noreply@github.com>2018-10-20 06:47:48 -0700
commita1c0a1ae5a63cee9cafe5edec48a0536ca5b7d6e (patch)
tree46189fb857aefc82ab5a5dbec1a0a9485c3fefe2
parent2242c42b977da6eaf8247877e1efd7327d0fd39c (diff)
parent4d2cca06662191d6f7012d01612d01ccde876dbe (diff)
Merge branch 'master' into fixNonDumpingfixNonDumping
-rw-r--r--.travis.yml7
1 files changed, 2 insertions, 5 deletions
diff --git a/.travis.yml b/.travis.yml
index a5d629215..265f42bb4 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -67,10 +67,7 @@ script:
makeCheck() {
cd build
make -j2 check ARGS='-LE regress[1-4]' CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED"
- }
- makeExamples() {
- cd build
- make -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";
+ ctest -j2 -L example || error "RUNNING EXAMPLES FAILED"
}
run() {
echo "travis_fold:start:$1"
@@ -80,7 +77,7 @@ script:
}
[ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker
[ -n "$TRAVIS_CVC4" ] && run configureCVC4
- [ -n "$TRAVIS_CVC4" ] && run makeCheck && run makeExamples
+ [ -n "$TRAVIS_CVC4" ] && run makeCheck
[ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration"
echo "travis_fold:end:load_script"
- echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback