# CONFIG_USB_OHCI_HCD_PLATFORM is not set