redundant;
authorwenzelm
Mon Nov 02 16:03:03 2015 +0100 (2015-11-02)
changeset 6154419d84de5f534
parent 61543 de44d4fa5ef0
child 61545 57000ac6291f
redundant;
src/Tools/jEdit/src/jedit_editor.scala
     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 =