src/Tools/jEdit/src/document_view.scala
changeset 55618 995162143ef4
parent 55432 9c53198dbb1c
child 55712 e757e8c8d8ea
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Feb 20 14:17:28 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Feb 20 14:36:17 2014 +0100
     1.3 @@ -243,7 +243,7 @@
     1.4            }
     1.5  
     1.6          case bad =>
     1.7 -          java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
     1.8 +          System.err.println("command_change_actor: ignoring bad message " + bad)
     1.9        }
    1.10      }
    1.11    }