# CONFIG_DVB_USB_DVBSKY is not set