> > > Please use @dots{} here and elsewhere, it looks better in print.
> > 
> > Should I use that in @smallexample too?
> 
> Sure, why not?

I was thinking that the @smallexample should probably be a verbatim
copy of debugger output, and so the style should be consistent. But
I used @dots like you said.

> > +is replaced by @dots{}.  In this case, the example above now becomes:
> 
> @code{@dots{}}

Oups, fixed.

> Otherwise, fine with me.  Thanks!

Thanks. Attached is what I ended up checking in. The NEWS change is
also now in.

Thanks for your help, Eli.
-- 
Joel