diff options
| author | Maxime Dénès | 2018-02-05 10:46:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-05 10:46:56 +0100 |
| commit | f5cf5e062bdc6264dc3c398ad76559ec188cde47 (patch) | |
| tree | 0d08db42279a4b937f2603bfd715bdb1ab597cd0 /dev/ci | |
| parent | f9818ce50dd25aa48101a0566184f75049dc37a3 (diff) | |
| parent | 67c16ccd3fd31f532f446d17c53837ac80e0b4a4 (diff) | |
Merge PR #6654: CI: Run coqchk on Iris
Diffstat (limited to 'dev/ci')
| -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 cf24d202d9..267e13359b 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 ) |