diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-20 06:47:30 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-20 06:47:30 -0700 |
| commit | 4d2cca06662191d6f7012d01612d01ccde876dbe (patch) | |
| tree | cac007e13bec7d9ed2a1d50a1819579c5dfaccd0 /.travis.yml | |
| parent | 6690518dee7cfa2dce3edec2ffc11e8780d41838 (diff) | |
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 7 |
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}" |