On Thu, 27 Apr 2023 12:50:07 GMT, Hannes Wallnöfer <hann...@openjdk.org> wrote:
> Please review a change to make JavaDoc search Unicode-aware and better handle > elements and index items with digits in their names. The most significant > change is to use Unicode property escapes in regular expressions in the > search script, but a few other changes were needed. In addition to running > the updated test I did extensive manual testing on multiple desktop and > mobile browsers to make sure search behavior did not change for other cases. This pull request has been closed without being integrated. ------------- PR: https://git.openjdk.org/jdk/pull/13690
