diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-bedrock2.sh | 11 |
2 files changed, 17 insertions, 0 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 2ebbf2cc4..28321d13e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -148,6 +148,12 @@ : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" ######################################################################## +# bedrock2 +######################################################################## +: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" + +######################################################################## # Equations ######################################################################## : "${Equations_CI_BRANCH:=master}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh new file mode 100755 index 000000000..447076e09 --- /dev/null +++ b/dev/ci/ci-bedrock2.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" + +git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" +( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) + +( cd "${bedrock2_CI_DIR}" && make ) |