aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-geocoq.sh
AgeCommit message (Expand)Author
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
2018-06-11[ci] GeoCoq now depends on math-comp's ssralg.Emilio Jesus Gallego Arias
2018-05-16[ci] Don't build lite versions of CI developments.Emilio Jesus Gallego Arias
2018-04-05Improve shell scriptszapashcanon
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
2017-03-10[travis] Move GeoCoq to allow fail.Emilio Jesus Gallego Arias
2017-03-02[travis] Backport trunk's travis support.Emilio Jesus Gallego Arias