/* Outputs a formatted string on the DBGU stream, using a variable number of arguments.  */
signed int printf(const char *pFormat,...)
/* Outputs a formatted string on the DBGU stream, using a variable number of arguments.  */
signed int printf(const char *pFormat,...)
{
    va_list ap;
    signed int result;
    va_start(ap, pFormat);
    result = vprintf(pFormat, ap);
    va_end(ap);
    return result;
}