From 5f26ee547a9976d1ccfe7cff22d886f7d7df1eef Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 26 Nov 2019 15:36:56 -0500
Subject: [ci] Split out the dependencies of fiat-crypto

---
 dev/ci/ci-bedrock2.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci/ci-bedrock2.sh')

diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2ac78d3c2b..8570c34194 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install )
-- 
cgit v1.2.3