Fixup the indentation of a comment that was mangled by pgindent, and

add dashes to the start/end of the comment block to try to prevent
this happening in the future.