src/Tools/jEdit/src/monitor_dockable.scala

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 24 13:32:51 2013 +0200
@@ -45,6 +45,7 @@
             rev_stats ::= props
             delay_update.invoke()
           }
+
         case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
       }
     }