Merged write-output-to-file [f=711548]

A new HTMLOutputMixin can be used with commands that generate output.
It allows them to define a '--output-file' or '-o' option that
contains the name of the file to write HTML contents to.  The
'generate-<board-type>' commands all use the mixin to provide this
behaviour.