From the history of the sources, it is clear that options.textarea.lineSpacing was originally not intended for negative values, but people started using it like that re-adjust fonts that appear a bit too high. Also note that modern displays often have 16x9 TV format, where vertical space is scarce: with negative line spacing a few more lines fit on the screen.
Many other jEdit componts and plugins have already been adapted to allow negative line spacing in the past 12 months.
It would be nice to have this important plugin within the club.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Hi, I'm not completely sure I understand, why would I use a negative value for lineSpacing ?
From the history of the sources, it is clear that options.textarea.lineSpacing was originally not intended for negative values, but people started using it like that re-adjust fonts that appear a bit too high. Also note that modern displays often have 16x9 TV format, where vertical space is scarce: with negative line spacing a few more lines fit on the screen.
Many other jEdit componts and plugins have already been adapted to allow negative line spacing in the past 12 months.
It would be nice to have this important plugin within the club.
I see, thanks