[Gretl-devel] Several things