# CONFIG_VIDEO_ALLEGRO_DVT is not set