On Sun, 29 Dec 2019, Mark Wielaard wrote: > Maybe we should have a separate historical git repo which contains > everything that we were able to salvage and that people could git > remote add if they are really, really interested.
I'm not convinced that's very different from having one repo with everything but some pieces in refs that aren't fetched by default. Maybe separate repos make fetching a bit more efficient if it allows packs to be reused on the server, but they also mean extra administrative overhead ensuring the correct configuration for each repo (for public access, not allowing pushes to the historical repo, etc.). -- Joseph S. Myers jos...@codesourcery.com
