Withdrawn: JDK-8303056: Improve support for Unicode characters and digits in JavaDoc search

[Hannes Wallnöfer]

On Thu, 27 Apr 2023 12:50:07 GMT, Hannes Wallnöfer <hannesw at 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