mirror of
https://github.com/koreader/koreader.git
synced 2025-08-10 00:52:38 +00:00
65ce72df27
We want to be able to set a custom value (i.e., more_options), because on high-dpi devices, the scaling can lead to pretty large differences; but more_options on a toggle is ugly and clunky. So, switch to something more suited to what this actually sets, which is ultimately an absolute pixel value, like margins. Add a few more steps on the low end to fill out the bar (and because that's where I found them most useful on high-dpi devices).