Re: @noindent without effect after @end smallexample

[Karl Berry]

    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