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] [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