Re: [Gretl-devel] tabbed editor: good news/bad news