--- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Apr 29 16:00:13 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Apr 29 16:00:34 2014 +0200
@@ -86,7 +86,7 @@
getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
getPainter.setStyles(
SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
- getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
+ getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
val fold_line_style = new Array[SyntaxStyle](4)
for (i <- 0 to 3) {