src/Tools/jEdit/src/document_view.scala
changeset 52767 9c28559e5fff
parent 52759 a20631db9c8a
child 52973 d5f7fa1498b7
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:37:59 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:43:21 2013 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     1.5      {
     1.6        // no robust_body
     1.7 -      model.flush()
     1.8 +      model.update_perspective()
     1.9      }
    1.10    }
    1.11