git: openjdk/mobile: 8223252: Update Javadoc help page with new search features

[duke]

Changeset: ff2f628e
Author:    Hannes Wallnöfer <hannesw at openjdk.org>
Date:      2019-12-02 18:52:18 +0000
URL:       https://git.openjdk.java.net/mobile/commit/ff2f628e

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