From 0e522231caca7874532735c61b7f57c13ea15704 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Otto=20Boly=C3=B3s?= <obolyos@mriiot.com>
Date: Sat, 9 Dec 2023 21:32:16 +0100
Subject: [PATCH] chore: add `styles/old` to `.dockerignore` (fix #375)

This folder is not necessary to copy to the Docker images.
---
 .dockerignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.dockerignore b/.dockerignore
index 32b9176c..a1298979 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -24,3 +24,4 @@ terms.tex
 
 *.log
 .DS_Store
+styles/old