aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-flocq.sh
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2020-11-26[ci] avoid always rebuilding jobs that use remakeEnrico Tassi
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-21Fix VST after PrincetonUniversity/VST#402Gaëtan Gilbert
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
2020-04-03Fix Flocq CI script.Théo Zimmermann
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
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-03-13[travis] Basic support for overlays.Emilio Jesus Gallego Arias
We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support.
2017-03-10[travis] Adding a template file and using it for all targets.Théo Zimmermann
2017-03-10[travis] Change headband for wider compatibility.Théo Zimmermann
2017-02-15[travis] [External CI] Factor out math-comp installs.Emilio Jesus Gallego Arias
We make math-comp overlays easier, we also start structuring the scripts a bit more.
2017-02-07[travis] Move ci files from `tools` to `dev`.Maxime Dénès