aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
Commit message (Collapse)AuthorAge
...
| * [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02
|
* [travis] [External CI] fiat-parsersGravatar Emilio Jesus Gallego Arias2017-02-24
|
* [travis] track an 8.7 specific branch of HoTT.Gravatar Maxime Dénès2017-02-21
| | | | This is required since we merged PR#309: Ltac as a plugin.
* [travis] [External CI] CompCert official 8.6 support + UniMathGravatar Emilio Jesus Gallego Arias2017-02-15
|
* [travis] [External CI] Factor out math-comp installs.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | | | | We make math-comp overlays easier, we also start structuring the scripts a bit more.
* Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileGravatar Maxime Dénès2017-02-07
|\
| * [travis] [External CI] [geocoq] don't build slow fileGravatar Emilio Jesus Gallego Arias2017-02-07
| | | | | | | | | | Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case.
* | [travis] [External CI] iris-coq: fix dependenciesGravatar Emilio Jesus Gallego Arias2017-02-07
|/
* [travis] [External CI] GeoCoqGravatar Emilio Jesus Gallego Arias2017-02-07
|
* [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07