>>>>> "Martin" == Martin Vermeer <[EMAIL PROTECTED]> writes:
>> Could also please make sure that the capitalization (ovalbox vs. >> Ovalbox) does not play a role? This is quite bad UI-wise. Martin> But it *does* play a role in LaTeX... Who is going to understand what ovalbox and Ovalbox do? what about giving them (at least in the UI) a reasonably descriptive name? JMarc
