diff options
| author |  Ralf Jung <post@ralfj.de> | 2018-01-31 20:22:19 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2018-01-31 20:22:19 +0100 |
| commit | 67c16ccd3fd31f532f446d17c53837ac80e0b4a4 (patch) | |
| tree | 573ac03c86b19b51297f86e3b73a4ff5b95bf9b7 /dev/ci/ci-iris-lambda-rust.sh | |
| parent | d0e05a1964fb2af093ac2a15a75bb84d342bf1ad (diff) | |
CI: Run coqchk on Iris
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index cf24d202d..267e13359 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -34,8 +34,8 @@ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_UR # Build std++ ( cd ${stdpp_CI_DIR} && make && make install ) -# Build iris -( cd ${Iris_CI_DIR} && make && make install ) +# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris +( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install ) # Build lambdaRust ( cd ${lambdaRust_CI_DIR} && make && make install ) |