aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-04-04 16:14:32 +0200
committerGaëtan Gilbert2019-04-04 16:14:32 +0200
commit2e1aa5c15ad524cffd03c7979992af44ab2bb715 (patch)
treeaeaead4a8729a46efcde0334b1a79a6422e760ad /dev
parent32080d6fe63f2af723decd618bdb8867703e084a (diff)
parent8e4004013182df73f0a0e8521583cd4f79a3ca66 (diff)
Merge PR #9904: [CI] Fix build of math-comp dependencies
Reviewed-by: SkySkimmer Reviewed-by: gares
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/ci-common.sh16
1 files changed, 9 insertions, 7 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b4d2a9ca4e..7aa265cf90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -108,10 +108,9 @@ install_ssreflect()
git_download mathcomp
- ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
- make Makefile.coq && \
- make -f Makefile.coq ssreflect/all_ssreflect.vo && \
- make -f Makefile.coq install )
+ ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \
+ make && \
+ make install )
}
@@ -123,8 +122,11 @@ install_ssralg()
git_download mathcomp
( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
- make Makefile.coq && \
- make -f Makefile.coq algebra/all_algebra.vo && \
- make -f Makefile.coq install )
+ make -C ssreflect && \
+ make -C ssreflect install && \
+ make -C fingroup && \
+ make -C fingroup install && \
+ make -C algebra && \
+ make -C algebra install )
}