[Gretl-devel] Re: rename small "extra" dir in git?