diff --git a/dist/tools/doccheck/check.sh b/dist/tools/doccheck/check.sh index 6cd2e6ec694d0b5420255f900f99322271b39d4e..b709cd7fcaaf958e0184f3a2f1bd08213b685db5 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