src/Tools/jEdit/src/pretty_text_area.scala
changeset 56360 1d122af2b11a
parent 56323 e925118b1875
child 56662 f373fb77e0a4
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 02 12:26:11 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 02 13:03:01 2014 +0200
@@ -85,6 +85,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))
 
     val fold_line_style = new Array[SyntaxStyle](4)
     for (i <- 0 to 3) {