From 174d058cbedad96c0a80da7787c88debd62d9496 Mon Sep 17 00:00:00 2001
From: Jaifroid <egk10@cam.ac.uk>
Date: Tue, 30 May 2023 16:49:56 +0100
Subject: [PATCH] Allow the dist folder to be included in gh-pages

---
 .github/workflows/publish-docker.yaml | 2 ++
 .gitignore                            | 1 -
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/publish-docker.yaml b/.github/workflows/publish-docker.yaml
index 14a27fe8..9b66e211 100644
--- a/.github/workflows/publish-docker.yaml
+++ b/.github/workflows/publish-docker.yaml
@@ -79,6 +79,8 @@ jobs:
           echo "Publishing to GitHub pages..."
           git config user.name "GitHub Actions Bot"
           git config user.email "<>"
+          # Delete gitignore entry for the dist folder
+          sed -i "/^\/dist\/$/d" .gitignore
           if [ ! -z "$(git status --porcelain)" ]; then
             git add .
             git commit -m "Set GitHub Pages release version"
diff --git a/.gitignore b/.gitignore
index 13001140..c9235cb7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,7 +5,6 @@
 _pkginfo.txt
 /bld/
 /bin/
-/dist/
 /BundleArtifacts/
 /dist/
 /archives/*.zim*