aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-04-20 16:17:36 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-04-20 16:17:36 -0400
commite81e281754d7f8c76b4e7767edcbcbc5b41afd6f (patch)
tree41a7638a8f0b7a360460f0146b7938222827a63a /dev
parent239e28f71192d7537bc6ea283c806ba28fa1c016 (diff)
[ci] Also make some display targets for fiat-crypto
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 6c8dce5bd..845addb4c 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -8,4 +8,4 @@ fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
-( cd "${fiat_crypto_CI_DIR}" && make lite )
+( cd "${fiat_crypto_CI_DIR}" && make lite lite-display )