gzip’ped instead of PKZIP’ped HTML (as an option)

[mirabilos]

If it’s not too much effort…

Looking at createHtmlBundle() I think the HTML export file itself is not cached, and the content is always just one file, so it should be possible to offer gzip(1)-compressed in addition to PKZIP-archived HTML. python3-gzip exists and even defaults to a suitable compression level (which, for gzip (in contrast to some others), is the highest).

This would help Unix users as it’s easier to decompress there (and, in fact, the browser can often do that… I know even MSIE 5 did that when it was not supposed to). I’d leave the PKZIP export in though for the “average desktop OS user”.

[iridescent-beacon]

This also seems reasonable and shouldn't be too much work. Will mostly be a test to see how hard I made it to extend the export type list :p

Will see about making this change over the weekend.