Preserve docker cache on unrelated changes

dmf-unicatt · Feb 12, 2024 · 6d3d0e4 · 6d3d0e4
1 parent d5d1742
commit 6d3d0e4
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/.dockerignore b/.dockerignore
@@ -0,0 +1,2 @@
+.git
+docker
diff --git a/patches/turing/apply_patches.sh b/patches/turing/apply_patches.sh
@@ -7,7 +7,7 @@
 
 set -e
 
-if [[ ! -e "docker" || ! -e "mathrace_interaction" || ! -e "patches" || ! -e "turing" ]]; then
+if [[ ! -e "mathrace_interaction" || ! -e "patches" || ! -e "turing" ]]; then
     echo "This script must be run as 'bash patches/turing/apply_patches.sh' from the top level directory of the repository"
     exit 1
 fi