# HG changeset patch
# User immler@in.tum.de
# Date 1243436822 -7200
# Node ID 7a0531f2be616ea6cfe84ecbcaa9a9e924bf3277
# Parent  aef72e071725505c15b2ac08bbb82967a82adaa7
no null change

diff -r aef72e071725 -r 7a0531f2be61 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed May 27 16:23:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed May 27 17:07:02 2009 +0200
@@ -216,8 +216,6 @@
                         cmd.markup_root += cmd.markup_node(begin.get, end.get, OuterInfo(kind))
                         command_change(cmd)
                       })
-                    else
-                      command_change(command)
                   case _ =>
                   //}}}
                 }