#include <stdint.h>

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

int32_t dev_ps2kb_read(int32_t *ch) {
  return ipcpipe(1, 0, IPCPIPE_READ, (uint8_t *)ch, sizeof(*ch));
}