From 4fd05b7cc58a8087baecd51b86603d3cf3f713d9 Mon Sep 17 00:00:00 2001
From: Hannah Bast <bast@informatik.uni-freiburg.de>
Date: Sat, 17 Aug 2024 13:31:25 +0200
Subject: [PATCH] Don't ignore `db` when building Docker image (#101)

We ignore this for our local image because there we mount the `db` directory as a volume. But for the Docker build and push action on GitHub, it should of course not be ignored. This should fix #99
---
 .dockerignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.dockerignore b/.dockerignore
index 52a4d3c..d075d5a 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -1,4 +1,4 @@
-db
+!db
 .git
 !.git/HEAD
 !.git/refs/heads