Closed makarius closed 11 years ago
In the extremes of font scaling, there should probably be some hard-coded limits. In Isabelle/jEdit the interval is 5..250 and the increment is scaled itself by size / 10. In Firefox the interval is even more narrow.
Thanks - done the same.
In the extremes of font scaling, there should probably be some hard-coded limits. In Isabelle/jEdit the interval is 5..250 and the increment is scaled itself by size / 10. In Firefox the interval is even more narrow.