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 "<* noreturn *>". > > Pushed. > > Gerald
apologies and thanks for correcting this bug regards, Gaius