summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-10-20 21:27:54 +0200
committerSon Ho2022-10-20 21:27:54 +0200
commitd62563cf9b8ef29ce20e810a5b1da999122c7a2f (patch)
tree45459740595bcdd70e5f4856b8499d1680d4ab91
parent6ca61f1deb2f2e45bf55c2b3fcf15b57a7b51ecb (diff)
Update the .gitignore
-rw-r--r--.gitignore4
1 files changed, 4 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index a90aa1fc..8713e6e4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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