HTMLify text logs

This makes an HTML version of every file in the executor log directory
with a ``.txt`` or ``.txt.gz`` extension.  If the original was
gzipped, the HTML version will be as well.