[Gretl-devel] a small generalization of the replace() interface