aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-common.sh
AgeCommit message (Expand)Author
2017-05-28Gitlab CIGaëtan Gilbert
2017-03-22[travis] Fix iris-coq build.Emilio Jesus Gallego Arias
2017-03-13[travis] Basic support for overlays.Emilio Jesus Gallego Arias
2017-03-10[travis] Make the git_checkout function more reliable.Théo Zimmermann
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
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
2017-02-07[travis] Move ci files from `tools` to `dev`.Maxime Dénès