aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-08-31 15:50:33 +0200
committerGaëtan Gilbert2018-08-31 15:50:33 +0200
commit166a3838a7f07df4181617e111ffeb67dd817929 (patch)
treebe9f362bcf1be7e44c5b0988c866c1a1fa292eec /dev/ci
parent066f39a306e7b3409355274b4b266ceda8de15ee (diff)
parent411cfb42e6ac9312a121886eaf4960369c992af0 (diff)
Merge PR #8346: Clean-up Travis folds.
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/ci-common.sh8
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'
-
}