Use .raw.html files from set.mm repository

[jkingdon]

Those are the copies that we have been maintaining, but until now what has been used in the live site are the copies from metamath-website-seed Assuming this works, we can remove the copies in metamath-website-seed which are out of date anyway.

There's a more full diagnosis at metamath/metamath-website-seed#14 (comment)

Steps:

1. get review on this pull request (ideally from @digama0 or @david-a-wheeler )
2. merge it
3. wait a day for the nightly website rebuild to happen
4. look at whether all 8 files are present in the generated site and whether they are the up to date copies from the set.mm repo
5. if yes, celebrate a little and figure we are good on mmil.html not updated #2
6. add nfegif/mmnf.raw.html to Remove files which live in set.mm repo metamath-website-seed#14 (the other seven files are already there)
7. move Remove files which live in set.mm repo metamath-website-seed#14 out of draft and merge it
8. wait a day for the nightly website rebuild to happen
9. make sure nothing broke in step 7 (it shouldn't have, but with these scripts you never know) by looking at whether all 8 files are present in the generated site

[jkingdon]

Are we OK to merge this? I don't have write access to this repository so I can't do it myself.

It strikes me as the fastest path to getting the web site updated. Right now https://us.metamath.org/ileuni/mmil.html still ends on phisum (over a year out of date) and the other web pages affected by this pull request have the same issue.

[digama0]

This PR is superseded by #16, which essentially rewrites the whole process and makes it much easier to review this kind of change. The current code in regenerate-website.sh is actually incorrect, it does the copying after running install.sh but this means that the copied files are not present in the mirrors or site zip.

[jkingdon]

This PR is superseded by #16, which essentially rewrites the whole process and makes it much easier to review this kind of change. The current code in regenerate-website.sh is actually incorrect, it does the copying after running install.sh but this means that the copied files are not present in the mirrors or site zip.

I don't have much of an opinion about how we fix it, so are we going to merge #16 ? I don't see any activity on that one in the last 3 weeks.

[digama0]

I was hoping to give some time for @david-a-wheeler or others to review it, but alas this may just be something we need to test in production.

[jkingdon]

I was hoping to give some time for @david-a-wheeler or others to review it, but alas this may just be something we need to test in production.

If need be I can come up with a serious answer to this, but for the moment I'll just post http://www.quickmeme.com/meme/22sv

[benjub]

I see above that this PR is superseded by #16 which has been merged. So, should this be closed ?

[jkingdon]

I see above that this PR is superseded by #16 which has been merged. So, should this be closed ?

Yes