diff options
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -34,6 +34,10 @@ rust-tests/target/ # F* .depend *.hints +tests/betree/obj/ +tests/hashmap/obj/ +tests/hashmap_on_disk/obj/ +tests/misc/obj/ # Misc /fstar-tests |