doc-gen icon indicating copy to clipboard operation
doc-gen copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Persistent scrollbars

Open pthomas505 opened this issue 5 years ago • 2 comments

I'm not sure if it is my browser (firefox), but the scrollbars have to be hovered over to make them appear. I was wondering if they could be changed to be persistent and maybe wider.

pthomas505 avatar Sep 13 '20 17:09 pthomas505

This behavior is due to these lines in style.css. (I've actually never noticed it since I'm using macOS and I changed its annoying default setting to only show scrollbars on hover.)

bryangingechen avatar Sep 13 '20 18:09 bryangingechen

Hiding the scrollbars (for the left and right navigation sidebar) was an intentional decision. I found it confusing to have 2 scrollbars on the right visible at all times. Zulip does the same BTW.

gebner avatar Sep 25 '20 07:09 gebner