diff options
| author | Son Ho | 2023-09-18 13:56:22 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-18 13:56:22 +0200 |
| commit | 38e5f64b598cce1f45c5831db58b77843d82041a (patch) | |
| tree | 28127f5c5d10fc0a2c57c425c045796f0c5d1d4e /backends/lean/.gitignore | |
| parent | 685391d3faa78d75f8d4bbded9cba12acbba5fcd (diff) | |
Cleanup the tutorial a bit
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions