Thank you Chris, this gave me the hint to find
Preferences chooseMenuFont
On 1/28/17, Chris Muller <
[hidden email]> wrote:
> Appearance | fonts | Menu font...
>
>
> On Sat, Jan 28, 2017 at 7:21 AM, H. Hirzel <
[hidden email]> wrote:
>> Hello
>>
>> How do I set the font size of the world menu and the docking bar menus?
>>
>> I found nothing in the preferences. Did this change?
>>
>> Regards Hannes
>>
>
>