-
Kurt Hindenburg authored
This replaces the text size slider by a number input w/ arrows. The slider is awkard to change the size. Instead of fixing the slider, the input arrows seem a better choice. The KIntNumInput has a slider that could be enabled we want to enable it. REVIEW: 105796
ebc594cd