using a batch file to correct the irritating html.html renaming is pretty
useless because a batch file could not edit eventual index.html files pointing
to an *html.html file.

This is really a nasty bug and an annoying feature. Who the hell decided a
mirror programming can change or add extensions to some other stuff?!