# CONFIG_IPMB_DEVICE_INTERFACE is not set