From c8a349766212b6909b577444f4d78e9828ad2dca Mon Sep 17 00:00:00 2001
From: Christian Helmuth <christian.helmuth@genode-labs.com>
Date: Thu, 16 Dec 2021 11:34:06 +0100
Subject: [PATCH] build: detect duplicates in REPOSITORIES

---
 tool/builddir/build.mk | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tool/builddir/build.mk b/tool/builddir/build.mk
index a991492f58..8c24d1a372 100644
--- a/tool/builddir/build.mk
+++ b/tool/builddir/build.mk
@@ -76,6 +76,15 @@ export BOARD
 REPOSITORIES := $(realpath $(shell echo $(REPOSITORIES)))
 BASE_DIR     := $(realpath $(shell echo $(BASE_DIR)))
 
+define nl
+
+
+endef
+
+ifneq ($(words $(REPOSITORIES)),$(words $(sort $(REPOSITORIES))))
+$(error detected duplicates in REPOSITORIES $(foreach p,$(REPOSITORIES),$(nl)    $(p)))
+endif
+
 #
 # Configure shell program before executing any shell commands. On Ubuntu the
 # standard shell is dash, which breaks colored output via its built-in echo