author | wenzelm |
Sat, 28 Aug 2010 17:37:57 +0200 | |
changeset 38842 | f762b33e0821 |
parent 38841 | 4df7b76249a0 |
child 38843 | d95522496593 |
--- a/src/Pure/System/session.scala Sat Aug 28 17:27:38 2010 +0200 +++ b/src/Pure/System/session.scala Sat Aug 28 17:37:57 2010 +0200 @@ -126,8 +126,6 @@ def handle_change(change: Document.Change) //{{{ { - require(change.is_finished) - val previous = change.previous.join val (node_edits, current) = change.result.join