aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-ltac2.sh
AgeCommit message (Expand)Author
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