Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Replace padding dots symbol by multiple dots (#16594)
Related to #16345. Summary of the issue: Multiple dots are reported as "padding dots" in situations where these dots have no padding function. "padding" is too restrictive and is also more difficult to understand; by the way, some translators have actually translated "padding dots" to "multiple dots" in their translations. Description of user facing changes Multiple dots (4 or more) will now be reported with the more neutral "multiple dots" instead of "padding dots" when the symbol level is high enough. Description of development approach Changed both the symbol name and what is reported in symbol file.
- Loading branch information