copy and paste from set.mm

[icecream17]

also fix typos in readme

migrates:
metamath/set.mm#2828
metamath/set.mm#2842
metamath/set.mm#2844
et al.

[icecream17]

does not resolve metamath/metamath-website-scripts#2
but still updates it to 2023, at least

---

^{(also my comment about how no one saw this is redacted)}

[benjub]

In my opinion, the *gif directories could be removed. They only create maintenance hassle.

[david-a-wheeler]

I think we need to raise dropping the gif-generated files, if that's the intent, on the Metamath mailing list. I'm find with doing that, I just want to make sure we have a general consensus before dropping them.

[david-a-wheeler]

I think mmil.raw.html should be exclusively in the set.mm repo, and removed from here.

This "seed" repo should have only the pages that aren't specific to any particular database.

[david-a-wheeler]

Hmm, we need to more clearly delineate what goes where.

My current thinking is that database-specific files go into the set.mm repo.

Files that aren't specific to any database, such as the top-level index.html file, go into seed.

I've just been alerted to a problem generating the files, so they're not getting the daily updates that is supposed to take place.

[david-a-wheeler]

So all the .raw.html files that you've edited should probably be removed from this repo (metamath-repo-seed) and only be edited in the set.mm repo. The top-level page (e.g., index.html for the very top of us.metamath.org) would go here in seed. Thoughts?

[benjub]

I agree with that separation; it is the most natural.

[jkingdon]

So all the .raw.html files that you've edited should probably be removed from this repo (metamath-repo-seed) and only be edited in the set.mm repo. The top-level page (e.g., index.html for the very top of us.metamath.org) would go here in seed. Thoughts?

I made #14 to do this. What I'm not sure I know enough to understand is whether this is all we need, or whether there is a script or permission or something which also needs to change to make this work.

[benjub]

Thanks @jkingdon. Then, we'll also have to merge both versions of index.html here and remove the version on the metamath/set.mm repo. Unfortunately, they already began to diverge (hopefully not too much), and I'm away from my main computer for the next ten days, so I won't be able to do it before then.

As stated above, I think we should remove support for the gif versions of the databases, to lower maintenance costs. We have to be reasonable: maintenance is already too heavy and the recent problems are a symptom that it is overwhelming.

[icecream17]

files are outdated + this pr will not be merged

[jkingdon]

files are outdated + this pr will not be merged

I confirmed that the files changed here have indeed been deleted from the metamath-website-seed repository.

So I agree with closing this pull request.