Re: [galaxy-dev] Setting extension of file names generated by Galaxy