diff options
Diffstat (limited to 'dev/ci/ci-mtac2.sh')
| -rwxr-xr-x | dev/ci/ci-mtac2.sh | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 1372acb8e5..7075d4d7f6 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,17 +3,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 +git_download unicoq -# Setup UniCoq +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) -git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" +git_download mtac2 -( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install ) - -# Setup MetaCoq - -git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}" - -( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) |