summaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorSon HO2024-06-22 15:07:14 +0200
committerGitHub2024-06-22 15:07:14 +0200
commit8719c17f1a363c0463d74b90e558b2aaa24645d6 (patch)
tree94cd2fb84f10912e76d1d1e8e89d8f9aee948f0c /scripts
parent8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (diff)
Do some cleanup in the Lean backend (#257)
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions