Merge pull request #10152 from miri64/tools/fix/doccheck

doccheck: exclude dist/tools directory from group check
This commit is contained in:
Alexandre Abadie 2018-10-11 16:13:30 +02:00 committed by GitHub
commit 26abf4cf8c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

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