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