aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-simple-io.sh
AgeCommit message (Collapse)Author
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
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-08-31[ci] Fix QuickChick by adding new simple-io dependency.Théo Zimmermann