| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-04-30 | renaming in Makefile.ci and ci scripts to avoid inconsistencies | Olivier Laurent | |
| 2020-04-21 | Fix VST after PrincetonUniversity/VST#402 | Gaëtan Gilbert | |
| Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257 | |||
| 2020-04-03 | Fix Flocq CI script. | Théo Zimmermann | |
| autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124 | |||
| 2018-08-31 | Download 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-05 | Improve shell scripts | zapashcanon | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |