Martin von Zweigbergk 4fb7dba73d repo: remove repo_path from ReadonlyRepo and RepoLoader
When loading repos on a server, there is no repo path. We currently
use a placeholder at Google. This patch will let us not do that.

I think we can remove the paths from `Workspace` too, but I'll leave
that for later, if at all.
2024-09-07 12:20:02 -07:00
..
2024-08-06 10:15:44 +09:00