src/Tools/jEdit/src/document_view.scala
changeset 64524 e6a3c55b929b
parent 64521 1aef5a0e18d7
child 64621 7116f2634e32
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 11:33:55 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 15:21:54 2016 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     1.5      {
     1.6        // no robust_body
     1.7 -      PIDE.editor.invoke_update()
     1.8 +      PIDE.editor.invoke_generated()
     1.9      }
    1.10    }
    1.11