It looks good.
Glad to hear it.
It is not completly clear that @noindent should
suppress the end of line, but since it seems to be what it does
historically lets not change it.@noindent doesn't suppress the end of line, exactly. It's more that it starts a paragraph. At least, text after the @noindent should not be ignored. Thanks, karl
