summaryrefslogtreecommitdiff
path: root/backends/lean/.gitignore
diff options
context:
space:
mode:
authorSon Ho2024-03-11 09:42:03 +0100
committerSon Ho2024-03-11 09:42:03 +0100
commit459a6e1297695c534e06f20cb53a19b3b576e588 (patch)
treec2c262bd86140a155fd1b082e1bc0e631f21cbac /backends/lean/.gitignore
parentbd6bd4158218c116cbb5a97a1ab8674175cdc773 (diff)
Update a builtin name
Diffstat (limited to 'backends/lean/.gitignore')
0 files changed, 0 insertions, 0 deletions