# CONFIG_DRM_MGA is not set