Re: Converting texinfo comments to HTML comments

[Karl Berry]

Hi Reinhold,

    are currently inside an @ignore block, so if it's not possible to convert 
    ignore blocks to comments, then we'll have to change a lot of files...)

I suppose it could be an option that you could enable, but I don't
think it should be done by default.  Comments and @ignore blocks are
there to be ignored, not to be propagated, seems to me ...

Of course there is 
@html
<!--
... git stuff ...
-->
@end html

I sympathize with your dilemma, but that would be the straightforward
way to do it, even though you have to "change a lot of files".

karl