How can I change the Latin font used for the line numbers at the top of vertical strokes? Thanks!
It's something which is likely to be done quite soon (let's say, in the next release), as it's a frequent request... besides, the user interface for this has been available for at least one or two years in JSesh (the inactive font menus in the preferences). A quick search on the web has allowed me to find one or two Java library to make a font chooser (amazingly, Java has no standard font chooser !), so it's very likely that I will do it.
It's something which is likely to be done quite soon (let's say, in the next release), as it's a frequent request... besides, the user interface for this has been available for at least one or two years in JSesh (the inactive font menus in the preferences). A quick search on the web has allowed me to find one or two Java library to make a font chooser (amazingly, Java has no standard font chooser !), so it's very likely that I will do it.
Serge Rosmorduc