src/Tools/jEdit/src/document_view.scala

--- a/src/Tools/jEdit/src/document_view.scala	Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Feb 20 14:36:17 2014 +0100
@@ -243,7 +243,7 @@
           }
 
         case bad =>
-          java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
+          System.err.println("command_change_actor: ignoring bad message " + bad)
       }
     }
   }