Open ethanwillis opened 5 months ago
If no one wants to take this on I'd actually like to submit a PR for this. But won't get around to it for a few hours.
That would be awesome! Thank you!
On Wed, Jan 24, 2024 at 6:18 PM Ethan Willis @.***> wrote:
If no one wants to take this on I'd actually like to submit a PR for this. But won't get around to it for a few hours.
— Reply to this email directly, view it on GitHub https://github.com/racket/drracket/issues/663#issuecomment-1909138024, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNME2AZFZGQUKJU2CNSDYQGQGDAVCNFSM6AAAAABCJTZUYWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMBZGEZTQMBSGQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>
I'm getting old and I enlarge my fonts. I noticed on the
preferences->colors->racket
screen the names of the items are not viewable if the editor font size is increased onpreferences->font
.Environment: Ubuntu 22.04. Linux, X+xfce 4.16.
Here are two screenshots. First is font size 14. Second is font size 24.