[Gretl-devel] decimal comma in GUI (was Re: Signalling)