diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-05 20:58:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:26:51 +0200 |
| commit | 88650b2e689972d79ea2d9bfad03366f1fca01a4 (patch) | |
| tree | 7d4166baa67438e468ab6bcf611e5b234f7e9aca /configure.ml | |
| parent | cde263581c49a75f8abdbcb398511942906e6204 (diff) | |
[gitlab] Do expensive builds with a flambda-compiled Coq.
Gains seem superior to 50%, but data is taken from Gitlab so no
reliable at all.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions