hg: jdk/jdk: 8223252: Update Javadoc help page with new search features

[hannes.wallnoefer at oracle.com]

Changeset: 2baa1f8721b8
Author:    hannesw
Date:      2019-12-02 18:52 +0100
URL:       https://hg.openjdk.java.net/jdk/jdk/rev/2baa1f8721b8

8223252: Update Javadoc help page with new search features
Reviewed-by: jjg

! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/formats/html/HelpWriter.java
! src/jdk.javadoc/share/classes/jdk/javadoc/internal/doclets/formats/html/resources/standard.properties