flush();
  public void write (int oneByte)  {    // We actually have to implement this method. Flush first so that    // things get written in the right order.    flush();    try      {        out.write (oneByte & 0xff);                if (auto_flush && (oneByte == '\n'))          flush ();      }    catch (IOException e)      {        setError ();      }  }