fix doc comment bug, noticed by Jochen