diff options
| author | Maxime Dénès | 2019-04-04 13:22:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-04 13:23:55 +0200 |
| commit | 8e4004013182df73f0a0e8521583cd4f79a3ca66 (patch) | |
| tree | aeaead4a8729a46efcde0334b1a79a6422e760ad /dev/ci | |
| parent | 32080d6fe63f2af723decd618bdb8867703e084a (diff) | |
[CI] Fix build of math-comp dependencies
We were incorrectly calling the global `install` target even when
building only subcomponents of the library.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-common.sh | 16 |
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 ) } |