# HG changeset patch
# User wenzelm
# Date 1355164136 -3600
# Node ID 53d3930dae0c0cb9fcc75044b9d7915d1bbb28e7
# Parent  0afb01666df2ef550455da5863ca141003ba3c89
keep diagnostic command -- avoid confusion when it disappears;

diff -r 0afb01666df2 -r 53d3930dae0c src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Mon Dec 10 19:17:16 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala	Mon Dec 10 19:28:56 2012 +0100
@@ -55,7 +55,6 @@
                 }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
-                try_replace_command(exec_id, "")
                 default_thread_pool.submit(() =>
                   {
                     val graph =