> > For that matter, I'm surprised that the editor and display fonts aren't > the same -- it's usually the same person using them both! > > > The ability to change the editor font was introduced by Mario a couple of > years ago: > > https://github.com/Jermolene/TiddlyWiki5/pull/2867 > > I think the rationale is that a monospaced editor font can make it easier > to work with wikitext markup. > > What I meant to write was that I was surprised that the *size* of the two font sets wasn't the same. It certainly makes sense to use a different font family for the tasks.
Thanks! -- You received this message because you are subscribed to the Google Groups "TiddlyWiki" 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/tiddlywiki/81d0affb-8fdd-484d-989c-ab0b3ac3cff5%40googlegroups.com.
