Re: [ jEdit-users ] Hack font

[maxwell <ma...@um...>]

On 2015-08-31 16:36, Dale Anson wrote:
> Steve, did you know you can adjust the vertical line spacing? It's in
> Utilities - Global Options - Text Area. The "Extra vertical line 
> spacing
> (in pixels)" can be set to a negative number. I set it to -2 for the 
> Hack
> font and now the line spacing looks about like it did with DejaVu.

Dunno about Steve, but I didn't realize that--and it gains me about 8 
lines of text on a good-sized monitor!

Another thing I didn't realize existed, but found when I was playing 
with this Hack font, is the ability to use "Additional fonts with font 
substitution" (in that same dialog box).  From what I can tell (I can't 
find it in the documentation), this means that code points that aren't 
covered in my default font will be filled in by another font that I 
specify.  (Just now tried it with a font that covers the Bengali 
script.)  Since I do a lot of multilingual computing, this will be very 
handy!

    Mike Maxwell