On Fri, Jul 05, 2019 at 11:09:09PM +0200, Mario Blättermann wrote: > readers think that the extension is hard coded to »gz«, and the > following explanation speaks about > »ext« which is nowhere to see in > the file name. I didn't think it was hard coded. Give us some credit, we're not all idiots.