#ifdef DECL_PRINTF
extern int printf (const char *, ...);
#endif