The only place the jEdit colorizer does anything about fonts is this:
def getFontFromParams(self, family: Any, size: Any, slant: Any, weight:
Any, defaultSize: int = 12) -> None:
return None
That is to say, it does nothing about getting or setting fonts.
--
You received this message because you are subscribed to the Google Groups
"leo-editor" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/leo-editor/320212e4-87fd-43d7-bb8e-0dff8d56fd20n%40googlegroups.com.
