Just noticed an annoying little bug:
turns out that HTML character codes -- which usually work on the nLab -- are not rendered if they appear inside an !include-d file.
A minimal (non-) working example is now in the Sandbox here:
https://ncatlab.org/nlab/show/Sandbox
(Sorry, I realize now that I am accidentally posting to the wrong site here.)
Just noticed an annoying little bug:
turns out that HTML character codes -- which usually work on the nLab -- are not rendered if they appear inside an !include-d file.
A minimal (non-) working example is now in the Sandbox here:
https://ncatlab.org/nlab/show/Sandbox
(Sorry, I realize now that I am accidentally posting to the wrong site here.)