1
0
mirror of https://github.com/RIOT-OS/RIOT.git synced 2025-12-26 23:11:19 +01:00

Merge pull request #10303 from cladmi/pr/make/docker/handle_worktree

makefiles/docker.inc.mk: handle building in git worktree
This commit is contained in:
Juan I Carrano 2018-10-31 15:39:31 +01:00 committed by GitHub
commit 77dc923d7e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -89,6 +89,11 @@ DOCKER ?= docker
DOCKER_VOLUMES_AND_ENV += $(if $(wildcard $(GIT_CACHE_DIR)),-v $(GIT_CACHE_DIR):$(DOCKER_BUILD_ROOT)/gitcache)
DOCKER_VOLUMES_AND_ENV += $(if $(wildcard $(GIT_CACHE_DIR)),-e GIT_CACHE_DIR=$(DOCKER_BUILD_ROOT)/gitcache)
# Handle worktree by mounting the git common dir in the same location
_is_git_worktree = $(shell grep '^gitdir: ' $(RIOTBASE)/.git 2>/dev/null)
GIT_WORKTREE_COMMONDIR = $(shell git rev-parse --git-common-dir)
DOCKER_VOLUMES_AND_ENV += $(if $(_is_git_worktree),-v $(GIT_WORKTREE_COMMONDIR):$(GIT_WORKTREE_COMMONDIR))
# This will execute `make $(DOCKER_MAKECMDGOALS)` inside a Docker container.
# We do not push the regular $(MAKECMDGOALS) to the container's make command in
# order to only perform building inside the container and defer executing any