https://sourceforge.net/p/drjava/support-requests/329/2016-09-14T11:23:47.134000ZRecent changes to 329: Menu font size2016-09-14T11:23:47.134000Z2016-09-14T11:23:47.134000ZBodreyhttps://sourceforge.net/u/bodrey2006/https://sourceforge.neta813e8e0e8aff01ddad33623990559a2e27c269e

<div class="markdown_content"><p>I suppose this support request could be interpreted as a feature request as well, but I digress... is there any way to increase the font size of DJ's menu items? They're so small. thx in advance!</p></div>