/* A preallocated null_file stream. */
extern null_file null_stream;
-extern void gdb_flush (ui_file *);
+extern void ui_file_flush (ui_file *);
extern int ui_file_isatty (struct ui_file *);
extern long ui_file_read (struct ui_file *file, char *buf, long length_buf);
+extern void ui_file_puts (struct ui_file *file, const char *buf);
+
extern int gdb_console_fputs (const char *, FILE *);
/* A std::string-based ui_file. Can be used as a scratch buffer for