From v5.5.0, If $HTMLEntities is
true, non-ASCII characters are encoded as numeric HTML entities (e.g. ૏). If $HTMLEntities is
false, non-ascii characters are exported as UTF-8 characters. Previously, these were not displayed in HTML View if the corresponding glyphs were not available in the chosen font. Tinderbox now uses fallback fonts to display these glyphs.