aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-coq-dpdgraph.sh
AgeCommit message (Collapse)Author
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
This is convenient as to have better automation.
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-08-01Have coq-dpdgraph ci test print the differencesJason Gross
This allows better debugging when it fails.
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-02Add coq-dpdgraph CIJason Gross