summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorSon Ho2023-05-07 16:46:43 +0200
committerSon HO2023-06-04 21:44:33 +0200
commitc09831bd1d935f06d8364ea0eb90df098d07e1aa (patch)
tree640620c1da69563ecb4b001cee49c2047a39b092 /.gitignore
parentb4a1f3233fb90cddbde63cbdf1d63785c81cc682 (diff)
Update Primitives.lean
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions