Thank you Chris, this gave me the hint to find

    Preferences chooseMenuFont



On 1/28/17, Chris Muller <asqueaker at gmail.com> wrote:
> Appearance | fonts | Menu font...
>
>
> On Sat, Jan 28, 2017 at 7:21 AM, H. Hirzel <hannes.hirzel at gmail.com> 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
>>
>
>