From 4a3f5abfa5cdbff1bbe5dd87b9101a66aea438ba Mon Sep 17 00:00:00 2001
From: Shish <shish@shishnet.org>
Date: Sun, 19 Jan 2025 23:46:11 +0000
Subject: [PATCH 1/2] [docker] exit early if build fails

If the build fails, don't then attempt to run the container-which-wasn't-built
---
 .devcontainer/build.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.devcontainer/build.sh b/.devcontainer/build.sh
index f7b640c0..10f8b69a 100755
--- a/.devcontainer/build.sh
+++ b/.devcontainer/build.sh
@@ -1,3 +1,4 @@
 #!/bin/sh
+set -eu
 cd $(dirname $0)/../
 docker run --rm -v ${PWD}:/app $(docker build -q -f .devcontainer/Dockerfile .)

From cc0feeed4c0176c12e557b9afe2e415acce7b3b4 Mon Sep 17 00:00:00 2001
From: Shish <shish@shishnet.org>
Date: Sun, 19 Jan 2025 23:46:19 +0000
Subject: [PATCH 2/2] [docker] mark doc directories as safe for git to use

docker mounting can cause the doc directory to be owned by a different user to the one running inside the container, which git complains about, but is fine for our use-case
---
 .devcontainer/Dockerfile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
index cea8fa13..11b726c0 100644
--- a/.devcontainer/Dockerfile
+++ b/.devcontainer/Dockerfile
@@ -3,6 +3,8 @@ ARG DEBIAN_FRONTEND=noninteractive
 ARG XDEBUG_MODE=coverage
 RUN apt update -y && apt install -y git composer php-cli php-dom php-curl php-xdebug vim
 WORKDIR /app
+RUN git config --global --add safe.directory /app/generator/doc/doc-en/en && \
+    git config --global --add safe.directory /app/generator/doc/doc-en/doc-base
 CMD cd /app/generator/doc && ./update.sh && \
     cd /app && composer install && \
     cd /app/generator && composer install && php ./safe.php generate