remove comma as name separator

Commas are most of the time used as a part of a name, not to
separate multiple names.

See also #2950.
This commit is contained in:
Sarah Hoffmann
2023-01-22 21:10:12 +01:00
parent 1de8bdaafe
commit fabe45f60a
2 changed files with 13 additions and 7 deletions

View File

@@ -38,6 +38,7 @@ sanitizers:
default-pattern: "[A-Z0-9- ]{3,12}"
- step: clean-tiger-tags
- step: split-name-list
delimiters: ;
- step: strip-brace-terms
- step: tag-analyzer-by-language
filter-kind: [".*name.*"]