# HG changeset patch
# User wenzelm
# Date 1446476583 -3600
# Node ID 19d84de5f534c14a7ac4aa8a62d623a7c5df1913
# Parent  de44d4fa5ef0cdda25d98db9a682758903617bde
redundant;

diff -r de44d4fa5ef0 -r 19d84de5f534 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:02:32 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:03:03 2015 +0100
@@ -41,7 +41,7 @@
         name => (name, Document.Node.no_perspective_text))
 
     val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
-    if (edits.nonEmpty) session.update(doc_blobs, edits)
+    session.update(doc_blobs, edits)
   }
 
   private val delay_flush =