texinfo bug or user error: dots inside example

[Janis Johnson]

Is this a bug in texinfo or a user error?  Is it safe to use "..."
within examples?  This is used several places in GCC documentation.

Janis Johnson
IBM Linux Technology Center


@settitle Example of problem with dots in example

@command{makeinfo} from Texinfo 4.2 generates @code{<small>} tags for
dots when used inside an example.

@example
test.o: ELF N32 MSB @dots{}
@end example

The same thing happens in inline code, as in @code{this @dots{} example}.

This isn't valid HTML 4.01, but then it doesn't seem valid to use
texinfo commands inside of an example, either.  Is this a user error?