diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-24 14:26:22 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-24 14:26:22 +0200 |
| commit | 484c40ac59269a2f6d6e77f81defc4067539f733 (patch) | |
| tree | 6b64107973a472666bcf66dbab97c7505ee11a07 /lakefile.lean | |
| parent | 32c44690f1895947dd8b5267b5570800cd6cdd0a (diff) | |
Minor: Fix indentation. Sorry.
Diffstat (limited to 'lakefile.lean')
0 files changed, 0 insertions, 0 deletions