/* Write one char to serial, must not trigger interrupt  */
void rt_hw_serial_putc(const char c)
/* Write one char to serial, must not trigger interrupt  */
void rt_hw_serial_putc(const char c)
{
    if (c == '\n')
        rt_hw_serial_putc('\r');
    while (!((*(RP)SEP6200_UART0_LSR) & 0x40));
    *(RP)(SEP6200_UART0_TXFIFO) = c;
}