# CONFIG_SERIO_GPIO_PS2 is not set