On Wed, 02 Oct 2019 09:07:38 -0700, Jim Kingdon <[email protected]> wrote: > Seems like a good plan. I assume the file size on these are fairly small, so > there's no particular need to think in terms of, say, a separate repository > or something even more fancy like git-lfs?
Correct, the files are small. Also, git only stores copies of files when they *change*, and these files would almost never change. So even though the "people/" directory would be included in each later version of set.mm, it wouldn't take significant additional space. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iFhnC-0004pE-0t%40rmmprod07.runbox.
