aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-engine_bench.sh
AgeCommit message (Collapse)Author
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
A few libraries in the CI don't compile with it (out of memory).
2020-05-19[ci] Add mit-plv/engine-benchJason Gross
This is a new development where I'm aggregating a specific set of benchmarks. It's intended to be relatively lightweight, taking only a handful of minutes. It's probably one of the few developments currently testing Ltac2.