# CONFIG_DEBUG_INFO_NONE is not set