# CONFIG_USB_WHCI_HCD is not set