jEdit (was: out of space on /root)

[Liam Proven]

On 21 March 2017 at 14:47, Ralf Mardorf <silver.bullet at zoho.com> wrote:
> How would you chose fonts that are more bold, without making all other
> fonts much too bold?


In a browser, I zoom the text so that fonts are at least 2 pixels
thick. (I do not own any hi-DPI screens). In Word or similar, I zoom
to max visible page width and then size the window appropriately. In
text mode editors, I resize the terminal window or change its
settings.

If necessary, in a terminal emulator, I select a bold font. If it's a
plain text editor then it won't be showing formatting so it doesn't
matter if it can't show bold separately.


-- 
Liam Proven • Profile: https://about.me/liamproven
Email: lproven at cix.co.uk • Google Mail/Talk/Plus: lproven at gmail.com
Twitter/Facebook/Flickr: lproven • Skype/LinkedIn/AIM/Yahoo: liamproven
UK: +44 7939-087884 • ČR/WhatsApp/Telegram/Signal: +420 702 829 053