diff options
| author | Son Ho | 2023-09-18 13:07:02 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-18 13:07:02 +0200 |
| commit | 985277c435feaafcdb034cd51ff113d67b9304a6 (patch) | |
| tree | fe0963c0977241bad2df4f24f6c965aebe46e3ba /backends/lean/.gitignore | |
| parent | ba215d5f7f2cd087e6b920e7ea1793e4b114a775 (diff) | |
Make minor modifications to the tutorial
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions