aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-ltac2.sh
Commit message (Expand)AuthorAge
* Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-12-21
* Fix a copy-paste error in ci-ltac2.Gravatar Théo Zimmermann2017-12-08
* [ci] Add Ltac2Gravatar Jason Gross2017-11-04