# CONFIG_DVB_PLATFORM_DRIVERS is not set