From 6f8fd1d6dfecb9d6362115223b430ae21394d308 Mon Sep 17 00:00:00 2001
From: Martine Lenders <m.lenders@fu-berlin.de>
Date: Thu, 11 Oct 2018 15:07:33 +0200
Subject: [PATCH] doccheck: exclude dist/tools directory from group check
---
dist/tools/doccheck/check.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/dist/tools/doccheck/check.sh b/dist/tools/doccheck/check.sh
index 6cd2e6ec69..b709cd7fca 100755
--- a/dist/tools/doccheck/check.sh
+++ b/dist/tools/doccheck/check.sh
@@ -32,7 +32,7 @@ then
fi
exclude_filter() {
- grep -v -e vendor -e examples -e tests
+ grep -v -e vendor -e examples -e tests -e "\<dist/tools\>"
}
# Check all groups are defined
--
GitLab