change_receiver: start only once (already done in actor function);
authorwenzelm
Tue, 02 Jun 2009 21:27:51 +0200
changeset 34583 17c83413b7fe
parent 34582 5d5d253c7c29
child 34584 3457ef52de04
change_receiver: start only once (already done in actor function);
src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 21:20:22 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 21:27:51 2009 +0200
@@ -106,7 +106,7 @@
         }
       }
     }
-  }.start
+  }
 
   def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
     changes match {