aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-bignums.sh
AgeCommit message (Collapse)Author
2020-03-31[ci] Run bignums' testsPierre Roux
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-04-05Improve shell scriptszapashcanon
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
2017-11-09Fix ci-bignums.sh "missing ]" error.Gaëtan Gilbert
It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
2017-06-13[travis] extra test ci-bignums (+factorize other scripts)Pierre Letouzey