# CONFIG_WDTPCI is not set