# HG changeset patch
# User wenzelm
# Date 1398780034 -7200
# Node ID f377ddf1cc522adeb0569f56fc9b6dbb88a5e302
# Parent  28ff163eefef87da5f1b4ab340f739e9aa193acf
tuned whitespace;

diff -r 28ff163eefef -r f377ddf1cc52 src/Tools/jEdit/src/pretty_text_area.scala
--- 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) {