diff options
Diffstat (limited to 'util/docker/Makefile')
| -rw-r--r-- | util/docker/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/util/docker/Makefile b/util/docker/Makefile index 77526bba5e..45562d7a7b 100644 --- a/util/docker/Makefile +++ b/util/docker/Makefile @@ -177,6 +177,7 @@ docker-jenkins-attach: test-docker docker-build-docs: test-docker docker-build-docs: + mkdir -p $(top)/Documentation/_build $(DOCKER) run -it --rm \ --user $(UID):$(GID) \ -v "$(top)/:/data-in/:ro" \ |