http://gcc.gnu.org/bugzilla/show_bug.cgi?id=50642 --- Comment #4 from Andreas Schwab <schwab@linux-m68k.org> 2011-10-07 16:33:46 UTC --- A @smallexample is supposed to be smaller than an @example.