src/Tools/jEdit/src/pretty_text_area.scala
changeset 60250 baf2c8fddaa4
parent 59286 ac74eedb910a
child 61193 dde5ecbd5e10
     1.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 03 20:04:38 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 03 20:21:25 2015 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4        jEdit.getColorProperty("view.gutter.focusBorderColor"),
     1.5        jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
     1.6        getPainter.getBackground)
     1.7 -    getGutter.setFoldPainter(getFoldPainter)
     1.8 +    getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
     1.9      getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
    1.10  
    1.11      if (getWidth > 0) {