stdio_flush() seems to do nothing and documentation is wrong

[ecurtz]

As far as I can tell out_flush() isn't implemented in any of the stdio drivers, so stdio_flush() doesn't actually do anything.

Also the comment in the header file for stdio_flush() is copy/pasted from stdio_init_all()

[wintersteiger]

+1. This is hugely annoying. I'm trying to log from both cores and multiple timers and no amount of flushing I do, the output is always some degree of garbled. For example:

auto_init_mutex(log_mtx);

void vllog(const char *fmt, va_list args) {
  mutex_enter_blocking(&log_mtx);
  printf("[%010llu] ", time_us_64());
  vprintf(fmt, args);
  printf("\n");
  fprintf(stdout, "\n");
  fflush(stdout);
  mutex_exit(&log_mtx);
}

None of printf("\n");, fprintf(stdout, "\n");, or fflush(stdout); makes sure that the output is in fact put out.

[peterharperuk]

I think this is fixed - can you retest?