diff options
| author | Gaëtan Gilbert | 2019-03-15 22:22:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-15 22:22:26 +0100 |
| commit | beaccf0befcc59178ca59913e63625fa42f6d186 (patch) | |
| tree | 2cbaaabdde55571a931710eb431c15b660cc3403 /kernel/reduction.ml | |
| parent | 2f4a2a7adfbf4831ee03310e9f918c7d49c8d991 (diff) | |
| parent | 32332758aaa5800b003cffd552cdc8ee7a2137c0 (diff) | |
Merge PR #9783: [ci] [gitlab] Replace YAML grafting by `extends: ` declaration.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions