aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-hott.sh
AgeCommit message (Expand)Author
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
2018-07-24[travis] Also run coqchk on HoTTJason Gross
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