search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Incorrect text on http://us2.metamath.org/ileuni/mmbiblio.html #762

Closed jkingdon closed 5 years ago

jkingdon commented 5 years ago

The page http://us2.metamath.org/ileuni/mmbiblio.html contains the text "Bibliographic Cross-Reference for the Higher-Order Logic Explorer" just above the table, and "Higher-Order Logic Explorer Page(s)" as a table header. In both cases "Higher-Order Logic Explorer" should be "Intuitionistic Logic Explorer".

I'm not sure where this text is stored. It seems like the WRITE BIBLIOGRAPHY command just generates the table itself, not this part of mmbiblio.html. Yet mmbiblio.html is not checked in to git, so maybe it is one of those files which isn't in git yet?

Reported by Gérard Lang.

nmegill commented 5 years ago

mmbiblio.html is generated from a template by metamath.exe. The template is somewhat "brittle" because metamath.exe expects a certain format and is normally never edited, so I haven't put it on GitHub yet. (It will go there eventually.) I fixed the template, and the next site build will have the correction.

For future reference, the template file is called mmbiblio_IL.html in the ilegif directory of the metamathsite.zip download from the Metamath Home Page.

jkingdon commented 5 years ago

Thanks for fixing this, and for the explanation of how that template works. "Eventually" sounds like a good time to get it into git, in the sense that I don't anticipate that it will change very often.