Jean-Marc Lasgouttes schrieb:
"Daniel" == Daniel Lohmann <[EMAIL PROTECTED]> writes:
Daniel> I would, however, also prefer to have a fixed font size for
Daniel> all ERTs
Some people who use ERT for short bits would not like to have it be of
the same fixed size. However, I think it could be a bit smaller (like
foot is smaller).
Well, "huge" ERTs would probably never make any sense. As ERTs are rendered
in a monospaced font, they always break over several lines. At least if
using a screen of affordable size :-)
I think a maximum size would be good.
Daniel
