util/docker/Makefile: Create Documentation/_build for docker-build-docs
If the host directory of a bind mount does not exist, Docker will create it. However, the newly created directory will be owned by root due to the Docker service running within a root context. The docker command in the recipe for docker-build-docs binds Documentation/_build to /data-out within the container, so if it doesn't already exist, the documentation builder will be unable to copy the HTML output into /data-out since it runs with the same UID and GID as the host user. By creating, if necessary, the _build directory before the `docker run` command, there should always be an existing directory owned by the host user for docker to bind /data-out to (ignoring the case of an existing _build directory the current user does not have permission to write to), avoiding the issue where it cannot write the output. TEST: make -C util/docker docker-build-docs completes without issues with and without an existing Documentation/_build directory Change-Id: I6be9bc1fdca48f4d924f5c07cc261189ab6862fd Signed-off-by: Nicholas Chin <nic.c3.14@gmail.com> Reviewed-on: https://review.coreboot.org/c/coreboot/+/81127 Reviewed-by: Felix Singer <service+coreboot-gerrit@felixsinger.de> Tested-by: build bot (Jenkins) <no-reply@coreboot.org> Reviewed-by: Martin L Roth <gaumless@gmail.com>
This commit is contained in:
parent
a49dafc7d2
commit
56c3444d85
@ -177,6 +177,7 @@ docker-jenkins-attach: test-docker
|
|||||||
|
|
||||||
docker-build-docs: test-docker
|
docker-build-docs: test-docker
|
||||||
docker-build-docs:
|
docker-build-docs:
|
||||||
|
mkdir -p $(top)/Documentation/_build
|
||||||
$(DOCKER) run -it --rm \
|
$(DOCKER) run -it --rm \
|
||||||
--user $(UID):$(GID) \
|
--user $(UID):$(GID) \
|
||||||
-v "$(top)/:/data-in/:ro" \
|
-v "$(top)/:/data-in/:ro" \
|
||||||
|
Loading…
x
Reference in New Issue
Block a user