diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-15 20:25:58 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-15 20:25:58 +0200 |
| commit | 66134227080c17094527f84a3e4a7c59698c5310 (patch) | |
| tree | de41a2c551512f09bd79a0569e84a4f95593111d /lean-toolchain | |
| parent | 745ed4f35baea4b1da38c5d8be6851d6c5c9e728 (diff) | |
Minor: Add some comments
Diffstat (limited to 'lean-toolchain')
0 files changed, 0 insertions, 0 deletions