Skip to content

Commit

Permalink
[docker] mark doc directories as safe for git to use
Browse files Browse the repository at this point in the history
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
  • Loading branch information
shish committed Jan 19, 2025
1 parent 4a3f5ab commit cc0feee
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .devcontainer/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit cc0feee

Please sign in to comment.