diff options
| author | Théo Zimmermann | 2020-05-13 19:57:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 19:57:49 +0200 |
| commit | f6c8f673a1637639ddaec8d208720f7428624124 (patch) | |
| tree | 25723b8ba8d119a1f6c587829035495b235d9a5c /dev/tools/pre-commit | |
| parent | 37b1a35e022a5fb7713e5a1eb5bfd671f1c88248 (diff) | |
| parent | b0e3404de4dff81680861517f70c496af1d92bbc (diff) | |
Merge sections on Variants and Private inductive types into new file.
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions