src/Pure/PIDE/query_operation.scala
changeset 55618 995162143ef4
parent 54640 bbd2fa353809
child 56299 8201790fdeb9
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Thu Feb 20 14:17:28 2014 +0100
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Thu Feb 20 14:36:17 2014 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4              case _ =>
     1.5            }
     1.6          case bad =>
     1.7 -          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
     1.8 +          System.err.println("Query_Operation: ignoring bad message " + bad)
     1.9        }
    1.10      }
    1.11    }