aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-quickchick.sh
AgeCommit message (Collapse)Author
2021-03-24CI Quickchick: don't install quickchick executable to opamGaëtan Gilbert
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
They should not be necessary today as they date from the shareable pre-artifact epoch, an incur in an slowdown.
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile.
2018-06-02QuickChick CILeonidas Lampropoulos