htif_putuchar 44 kernel/arch/riscv64/include/arch/drivers/ucb.h extern void htif_putuchar(outdev_t *, const char32_t); htif_putuchar 44 kernel/arch/riscv64/src/drivers/ucb.c .write = htif_putuchar,