diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-26 19:07:36 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-26 19:07:36 +0200 |
| commit | 3bdc50ac878c1b6d066a342d2b4909b1b4e841d9 (patch) | |
| tree | 7c3faeb992f4bc3a7dfe0204d3803af25c6d8827 /lakefile.lean | |
| parent | a9ff650577b0b9c35066875d2dce7b4a72e0cb55 (diff) | |
Minor
Diffstat (limited to 'lakefile.lean')
0 files changed, 0 insertions, 0 deletions