Good catch Alex, thank you for testing this.

On Oct 9, 2019, at 11:33 AM, Alex Buckley <[email protected]> wrote:

I think #2 has a serious problem. If you scroll, and then hit any key,
then the search box grabs focus -- this is useful on the many occasions when 
you want to search, but it means that keyboard shortcuts such as Ctrl-C are 
pre-empted. Specifically, if I select text anywhere on the javadoc page with 
the mouse, then press Ctrl-C, I see focus jump to the search box; if I then 
switch to another program to paste in the copied text (to quote it in an email, 
say), then I find the clipboard is empty, nothing was copied, Ctrl-C was 
pre-empted. For this reason, I disregard #2.

Reply via email to