#ifndef __user_stdio
#define __user_stdio

extern u16 TXDMode;

void put_one_char(char c, void *dummy);
int printf(const char *format, ...);
#endif