summaryrefslogtreecommitdiff
path: root/backends/lean/.gitignore
diff options
context:
space:
mode:
authorSon Ho2023-09-18 13:56:22 +0200
committerSon Ho2023-09-18 13:56:22 +0200
commit38e5f64b598cce1f45c5831db58b77843d82041a (patch)
tree28127f5c5d10fc0a2c57c425c045796f0c5d1d4e /backends/lean/.gitignore
parent685391d3faa78d75f8d4bbded9cba12acbba5fcd (diff)
Cleanup the tutorial a bit
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions