#include <stdint.h>
#include <system/system.h>
#include <sysdefs/ipcpipe.h>
#include <printf/printf.h>

void putchar_(char c) {
  char buf = c;
  ipcpipe(IPCPIPE_SELFPID, IPCPIPE_OUT, IPCPIPE_WRITE, (uint8_t *)&buf, sizeof(buf));
}