src/Tools/jEdit/src/jedit_editor.scala
changeset 61544 19d84de5f534
parent 61011 018b0c996b54
child 61557 f6387515f951
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:02:32 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:03:03 2015 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4          name => (name, Document.Node.no_perspective_text))
     1.5  
     1.6      val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
     1.7 -    if (edits.nonEmpty) session.update(doc_blobs, edits)
     1.8 +    session.update(doc_blobs, edits)
     1.9    }
    1.10  
    1.11    private val delay_flush =