diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 9259a6e0c8..c379a01767 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -84,7 +84,7 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + echo 'Installing ssreflect' git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" @@ -93,14 +93,12 @@ install_ssreflect() make -f Makefile.coq ssreflect/all_ssreflect.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssr.install\\r' - } # this installs just the ssreflect + algebra library of math-comp install_ssralg() { - echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + echo 'Installing ssralg' git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" @@ -109,6 +107,4 @@ install_ssralg() make -f Makefile.coq algebra/all_algebra.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssralg.install\\r' - } |