aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-hott.sh
AgeCommit message (Expand)Author
2018-04-05Improve shell scriptszapashcanon
2017-12-21Fix CI with parallel make (messed up dependencies)Gaƫtan Gilbert
2017-07-21Alternate way of doing timing on ciJason Gross
2017-07-21Separate make from python script for HoTTJason Gross
2017-07-21Display timing data travis for various projectsJason Gross
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
2017-03-02[travis] Backport trunk's travis support.Emilio Jesus Gallego Arias