search: do not store repo name in progress.Stats.Repos (!27903) · Merge requests · Administrator / sourcegraph

Administrator requested to merge k/display-limit-4 into main Nov 18, 2021

Created by: keegancsmith

This is now just a set of repository IDs since we have removed all dependencies on the name. This should allow us to do further simplifications / prevent new dependencies on the name in the future.

Part of https://github.com/sourcegraph/sourcegraph/issues/27421

search: do not store repo name in progress.Stats.Repos

Merge request reports