#ifdef DECL_FPRINTF
extern int fprintf (FILE *, const char *, ...);
#endif