aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-hott.sh
Commit message (Expand)AuthorAge
* Improve shell scriptsGravatar zapashcanon2018-04-05
* Fix CI with parallel make (messed up dependencies)Gravatar Gaƫtan Gilbert2017-12-21
* Alternate way of doing timing on ciGravatar Jason Gross2017-07-21
* Separate make from python script for HoTTGravatar Jason Gross2017-07-21
* Display timing data travis for various projectsGravatar Jason Gross2017-07-21
* Remove -j ${NJOBS} from make invocations in the ciGravatar Jason Gross2017-06-16
* [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
* [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02