summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-11-27 14:15:01 +0100
committerSon Ho2023-11-27 14:15:01 +0100
commita17eef1053909117d75c9ea8eeaad786626cc05d (patch)
tree4de215bcf14c54eb653095c7ac398b0be10f87de /backends/lean
parentfdb8555cf6bc21ea230141373920196b078bdd28 (diff)
Update the way the Primitives file is copied
Diffstat (limited to 'backends/lean')
0 files changed, 0 insertions, 0 deletions