Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Custom fonts in browser_info html?

Email Gateway (Aug 23 2022 at 08:50):

From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
Is there an approved/supported facility for handling symbol glyphs from custom fonts in the html generated in the html files generated by
"build -o browser_info”?

At first blush it seems to ignore the font information in the symbols file and just expects the glyph to be in IsabelleDejaVuSansMono.ttf.

Last updated: Nov 21 2024 at 12:39 UTC