summaryrefslogtreecommitdiff
path: root/backends/lean/.gitignore
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-27 17:51:50 +0200
committerAymeric Fromherz2024-05-27 17:51:50 +0200
commit309435d24edb689736da83025eb08a6761b28b8b (patch)
treed1dfc5d42df9eca177cd69305f9efa69e3a4fec7 /backends/lean/.gitignore
parentc236ccfb22e64f56f4398d067582ebd570bf1a0b (diff)
Split collapse into collapse and reduce, rename accordingly
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions