diff options
| author | Emilio Jesus Gallego Arias | 2019-03-15 19:26:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-15 19:30:38 +0100 |
| commit | 32332758aaa5800b003cffd552cdc8ee7a2137c0 (patch) | |
| tree | 2cbaaabdde55571a931710eb431c15b660cc3403 /kernel/reduction.ml | |
| parent | 2f4a2a7adfbf4831ee03310e9f918c7d49c8d991 (diff) | |
[ci] [gitlab] Replace YAML grafting by `extends: ` declaration.
This should in general be more robust as we don't need to remember to
graft subsections.
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions