> On Nov 22, 2022, at 3:59 PM, Mario Carneiro <[email protected]> wrote:
>
> I think we should not put everything in set.mm repo, or if we do, we clearly
> separate set.mm from the rest of it. I think there is already too much stuff
> in the repo that isn't about set.mm itself. What you have described clearly
> sounds like a separate project, like a blog post series or something, and as
> such it wouldn't need to stay rigidly in sync and could just pin a version of
> set.mm to work with.
I agree with your general point of "don't put everything in the set.mm repo".
However, I have in mind a book that syncs with set.mm, that is, the book is
updated as set.mm changes, that is, it *DOES* stay rigidly in sync. The easiest
way to simultaneously edit them is to put them in the same repo :-).
---- 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/067489BC-395A-4AC3-AB27-5D632D09B4DE%40dwheeler.com.
