From c26710ac7e8d5edbe41f0d746a1ff119822eb75f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Harter?= <gaetan.harter@fu-berlin.de>
Date: Mon, 9 Sep 2019 17:52:54 +0200
Subject: [PATCH] makefiles/docker: handle mounting 'BOARDSDIR'

Handle setting 'BOARDSDIR' when building in docker.
---
 makefiles/docker.inc.mk | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/makefiles/docker.inc.mk b/makefiles/docker.inc.mk
index 4f053f3f67..b4055b8faf 100644
--- a/makefiles/docker.inc.mk
+++ b/makefiles/docker.inc.mk
@@ -251,6 +251,12 @@ DOCKER_VOLUMES_AND_ENV += $(if $(wildcard $(GIT_CACHE_DIR)),-e 'GIT_CACHE_DIR=$(
 DOCKER_VOLUMES_AND_ENV += $(call docker_volumes_mapping,$(EXTERNAL_MODULE_DIRS),$(DOCKER_BUILD_ROOT)/external,)
 DOCKER_OVERRIDE_CMDLINE += $(call docker_cmdline_mapping,EXTERNAL_MODULE_DIRS,$(DOCKER_BUILD_ROOT)/external,)
 
+# Remap 'BOARDSDIR' if it is external
+DOCKER_VOLUMES_AND_ENV += $(call docker_volumes_mapping,$(BOARDSDIR),,boards)
+# Value is overridden from command line if it is not the default value
+# This allows handling even if the value is set in the 'Makefile'.
+DOCKER_OVERRIDE_CMDLINE += $(if $(findstring $(RIOTBOARD),$(BOARDSDIR)),,$(call docker_cmdline_mapping,BOARDSDIR,,boards))
+
 # External module directories sanity check:
 #
 # Detect if there are remapped directories with the same name as it is not handled.