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

doccheck: exclude dist/tools directory from group check

This commit is contained in:
Martine Lenders 2018-10-11 15:07:33 +02:00
parent 239b3dfe86
commit 6f8fd1d6df

View File

@ -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