summaryrefslogtreecommitdiff
path: root/tests/fstar/.gitignore
diff options
context:
space:
mode:
authorSon Ho2023-08-07 08:59:27 +0200
committerSon Ho2023-08-07 08:59:27 +0200
commit987dc5c25a1d5cee19f4bba2416cbfa83e6ab6de (patch)
treec45ee0739f4dc64221a16ca0dcc0a0703758bd60 /tests/fstar/.gitignore
parenta106d3170eb784d23cd3614a21ef8f1bbb3be2f4 (diff)
Change some fun id names to use "Mut"/"Shared" as a suffix
Diffstat (limited to 'tests/fstar/.gitignore')
0 files changed, 0 insertions, 0 deletions