| changeset 73343 | d0378baf7d06 |
| parent 73340 | 0ffcad1f6130 |
| child 75393 | 87ebf5a50283 |
--- a/src/Tools/jEdit/src/font_info.scala Mon Mar 01 22:37:33 2021 +0100 +++ b/src/Tools/jEdit/src/font_info.scala Mon Mar 01 22:50:00 2021 +0100 @@ -22,7 +22,7 @@ val min_size = 5 val max_size = 250 - def restrict_size(size: Float): Float = size max min_size min max_size + def restrict_size(size: Float): Float = size max min_size.toFloat min max_size.toFloat /* main jEdit font */