From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 20 Oct 2018 13:47:30 +0000 (-0700)
Subject: Travis: run examples and avoid building them twice (#2663)
X-Git-Tag: cvc5-1.0.0~4396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d2cca06662191d6f7012d01612d01ccde876dbe;p=cvc5.git

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.
---

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}"