jEdit (was: out of space on /root)

[Colin Law]

On 21 March 2017 at 13:47, Ralf Mardorf <silver.bullet at zoho.com> wrote:
> On Tue, 21 Mar 2017 14:32:58 +0100, Liam Proven wrote:
>>>> http://www.xen.dds.nl/f/i/screenshots/jedit-5.1_from_Linux_over_X.png
>>> Not sure what you are complaining about exactly. it looks ok to my
>>> ancient eyes.
>>
>>Looks fine to me, too.
>>
>>The fonts are thinner than I'd like, so I'd choose a heavier font
>>size, but they're clear and sharp.
>
> How would you chose fonts that are more bold, without making all other
> fonts much too bold?
>
> I wonder that nobody complains about the sawtooth. Take a look at the
> chars "v" and "/".
>
> I dislike blurry fonts, but fonts that sharp, that you could see
> sawtooth isn't something I like either.

Are you talking about the menu labels along the top? You know you can
change the font in the edit window. However menu labels don't look
like that I don't think.
https://www.dropbox.com/s/0zn5tejo46vh8ie/jEdit.png?dl=0

Colin