diff options
| author | Son Ho | 2023-11-16 10:13:28 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-16 10:13:28 +0100 |
| commit | a27efd1ed08bc9583752445d9eda7a693c0c7379 (patch) | |
| tree | 5a3d1f1522cf813522798bb9bfd43d928b0b88e9 /backends/lean/.gitignore | |
| parent | e0351ad287332d5d1c71cee6a834f775db98966d (diff) | |
Finish propagating the changes to the names and cleaning
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions