doc-gen4
doc-gen4 copied to clipboard
Input focus is stolen by left or right column
I often press space in my web browser to go a page down, and shift+space to go a page up. These shortcuts don't appear to be working on pages such as https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Basic.html#PartialOrder.lift when I previously clicked a link in either nav column to the left or to the right.
It's a small inconvenience, but I'd prefer it if the navbars wouldn't steal the "input focus" so that my browser always does the PageDn in the middle column.
I understand the inconvenience, but I'd be hesitant to change this. IMO, the left and right navbars should remain scrollable with the keyboard for accessibility reasons.