> On Dec 6, 2021, at 4:44 PM, 'Alexander van der Vekens' via Metamath
> <[email protected]> wrote:
>
> Maybe we can find a compromise between David's (and my) proposal to have a
> separate file and Norm's proposal to keep only the recent changes in set. mm:
> Every time (year) the old entries are removed from set.mm, these entries are
> added to the history file. By this, we avoid (regularily) maintaining a
> separate file, which seems to be impractical, keep set.mm short and retain
> the whole history.
I'd be delighted to see that. Maybe call it "older_changes" or something like
that.
--- 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/B468ACEC-969A-49C9-B776-090BCACAD9E7%40dwheeler.com.
