On Tue, 19 Apr 2022 21:04:04 GMT, Hannes Wallnöfer <hann...@openjdk.org> wrote:
>> This is the second of two PRs to enhance JavaDoc search, it is based on the >> first one (#8185). >> >> It adds a standalone search page (search.html) along with its own script >> file (search-page.js). This PR is very similar to the last prototype I >> uploaded and demoed, the changes are mostly tweaks to the markup, style >> sheets and text. >> >> JDK API docs rendered with this patch can be viewed and tested here >> (top-level files only, updated on April 20th): >> http://cr.openjdk.java.net/~hannesw/8248863/api.02/ >> http://cr.openjdk.java.net/~hannesw/8248863/api.02/search.html > > Hannes Wallnöfer has updated the pull request incrementally with two > additional commits since the last revision: > > - Use different max results values for popup and page search > - Fix search link height The dependent pull request has now been integrated, and the target branch of this pull request has been updated. This means that changes from the dependent pull request can start to show up as belonging to this pull request, which may be confusing for reviewers. To remedy this situation, simply merge the latest changes from the new target branch into this pull request by running commands similar to these in the local repository for your personal fork: git checkout JDK-8248863 git fetch https://git.openjdk.java.net/jdk master git merge FETCH_HEAD # if there are conflicts, follow the instructions given by git merge git commit -m "Merge master" git push ------------- PR: https://git.openjdk.java.net/jdk/pull/8226
