Revert unfortunate whitespace change

In e5e2fc84, blank lines were removed
after a comment block, which now looks as though the comment refers to
the immediately following code, but it actually refers to the
preceding code.  So put the blank lines back.