You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: