Re: [Gretl-users] Anybody else with menu problems on Ubuntu 18.04?