Bug fix caused by a typo

Accidentally added two bits of "* */" while closing
a comment, which has now been removed.