aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-ltac2.sh
AgeCommit message (Expand)Author
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaëtan Gilbert
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
2018-04-05Improve shell scriptszapashcanon
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
2017-12-08Fix a copy-paste error in ci-ltac2.Théo Zimmermann
2017-11-04[ci] Add Ltac2Jason Gross