svoid drainStreamToPrint_charByChar(InputStream stream, IF0<Bool> enabled) {
  InputStreamReader in = new(process.getInputStream());
  int c;
  while ((c = in.read()) >= 0) {
    if (enabled == null || enabled!)
      print_noNewLine(str((char) c));
  }
}