diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-25 09:47:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-25 09:47:12 -0700 |
| commit | 4f384b6fadd999324d83b4c4ea900de2a0e13dd7 (patch) | |
| tree | d62683a66ede8c7a0ee04e8b67ee999aa71342ea /.travis.yml | |
| parent | f892370a615ecadc011b49a98d2c4695fafa7f4f (diff) | |
Use separate CMake project for CVC4 examples. (#3196)
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml index d4de3576c..64dd17c75 100644 --- a/.travis.yml +++ b/.travis.yml @@ -59,7 +59,13 @@ 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" - ctest -j2 -L example || error "RUNNING EXAMPLES FAILED" + } + makeExamples() { + cd examples + mkdir build + cd build + cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake + ctest -j2 --output-on-failure || error "RUNNING EXAMPLES FAILED" } makeInstallCheck() { cd build @@ -78,7 +84,7 @@ script: [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker [ -n "$TRAVIS_CVC4" ] && run configureCVC4 [ -n "$TRAVIS_CVC4" ] && run makeCheck - [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck + [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck && run makeExamples [ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration" echo "travis_fold:end:load_script" - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}" |