diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-09 15:24:01 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-09 15:24:01 +0200 |
| commit | 372737ba74baa2af8ee798df1b2768a5d827a179 (patch) | |
| tree | 3c81b58f6257abd797f2d015d467036537dd31a3 /Makefile.ci | |
| parent | e922afb970cee19a8421a6fa5f246c74a7ee8856 (diff) | |
| parent | 88650b2e689972d79ea2d9bfad03366f1fca01a4 (diff) | |
Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions