diff options
| author | Théo Zimmermann | 2018-08-28 16:59:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-28 16:59:15 +0200 |
| commit | 411cfb42e6ac9312a121886eaf4960369c992af0 (patch) | |
| tree | cddb3e70b1a438ff3376919e9cf652c26c1e4cdc /dev/ci | |
| parent | a57891211e578605f6cb7e05f5fdadd7de49e519 (diff) | |
Clean-up Travis folds.
This has become mostly garbage since GitLab CI became our main CI platform.
Diffstat (limited to 'dev/ci')
| -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' - } |
