[PATCH] Small (visual) issue in generating html documentation