diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 19:52:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 19:52:17 +0200 |
| commit | f01a1e45902bcd7ee077ead7037c809d776f35d2 (patch) | |
| tree | af65cfaa3463bf0711f037935b7735ce9a6713a9 /dev/ci/ci-common.sh | |
| parent | aca979230e6ff72913c63b844954f1ec9dc24d61 (diff) | |
| parent | ed91bf1fce168026675f986a0069ca596ad2b806 (diff) | |
Merge PR #7514: [ci] Don't build lite versions of CI developments.
Diffstat (limited to 'dev/ci/ci-common.sh')
| -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 2a14ed352..f867fd189 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -71,11 +71,6 @@ git_checkout() echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } -checkout_mathcomp() -{ - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}" -} - make() { # +x: add x only if defined @@ -93,7 +88,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp "${mathcomp_CI_DIR}" + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ |