[Gretl-devel] Re: naming of help menu entries