diff options
Diffstat (limited to 'dev/ci/ci-equations.sh')
| -rwxr-xr-x | dev/ci/ci-equations.sh | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 98735b4ec4..998d50faa7 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Equations_CI_DIR="${CI_BUILD_DIR}/Equations" +git_download Equations -git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}" - -( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) +( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ + make && make test-suite && make examples && make install) |