On Fri, 18 Nov 2022 21:37:04 GMT, Pavel Rappo <[email protected]> wrote:
>> Jonathan Gibbons has updated the pull request incrementally with one
>> additional commit since the last revision:
>>
>> Fix man page header
>
> src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/toolkit/BaseConfiguration.java
> line 520:
>
>> 518: * @return an array of tokens
>> 519: */
>> 520: private List<String> tokenize(String s, int maxTokens) {
>
> Not saying that we should do anything about it, but I would be surprised if
> there were no such tokenization functionality in the JDK API.
None of the JDK simple tokenizers supports handling of escape characters.
But a Pattern/Matcher could be used.
-------------
PR: https://git.openjdk.org/jdk/pull/11178
