docker: do not copy benchmarks dir (#59)

This should help making the Docker image a bit smaller.
Veridise · Oct 16, 2023 · ac5abf1 · ac5abf1
1 parent 976a14d
commit ac5abf1
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.dockerignore b/.dockerignore
@@ -1,2 +1,3 @@
 **/compiled
 .git
+benchmarks/