Gerald Pfeifer <ger...@pfeifer.com> writes:

> Note that in HTML < and > have a special meaning, so we cannot simply 
> write "<* noreturn *>", but need to escape it as "&lt;* noreturn *&gt;".
>
> Pushed.
>
> Gerald

apologies and thanks for correcting this bug

regards,
Gaius

Reply via email to