diff options
| author | Andreas Grois <andi@grois.info> | 2025-01-13 23:32:16 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-01-13 23:32:16 +0100 |
| commit | c6e82da892f8ee79881a8dafa3c01f7c7a682ae5 (patch) | |
| tree | c9e0cbeb5ac8bf48fce53dc8fea32076e1a2e5b7 /lakefile.lean | |
| parent | 55c2353f7c209538f1421d5775afd38e6d2f0e6a (diff) | |
Minor
Diffstat (limited to 'lakefile.lean')
0 files changed, 0 insertions, 0 deletions