aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-common.sh
AgeCommit message (Collapse)Author
2017-05-28Gitlab CIGaëtan Gilbert
2017-03-22[travis] Fix iris-coq build.Emilio Jesus Gallego Arias
We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
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] Make the git_checkout function more reliable.Théo Zimmermann
This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary).
2017-03-10[travis] Change headband for wider compatibility.Théo Zimmermann
2017-03-10Improve build of travis target on local machine.Théo Zimmermann
- Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date).
2017-02-15[travis] [External CI] CompCert official 8.6 support + UniMathEmilio Jesus Gallego Arias
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