diff options
| author | Tom Smeding <tom.smeding@gmail.com> | 2020-05-23 11:38:35 +0200 |
|---|---|---|
| committer | Tom Smeding <tom.smeding@gmail.com> | 2020-05-23 11:38:35 +0200 |
| commit | f85f5515486504c9c3401332269a0dda20c96f1d (patch) | |
| tree | e5bfbc0f80b23e6690a9d0e9c6e17ffb7fc135b7 /.gitignore | |
| parent | c3a2389203e743c874bb464c9343a2f0aab3ae62 (diff) | |
Also case-reduce in a case-scrutinised expression
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions