[Gretl-devel] trivial stuff