#ifdef DECL_FFLUSH
extern int fflush (FILE *);
#endif