Martin Vermeer <[EMAIL PROTECTED]> writes: > Yes... and less intrusive for now. > > But is this actually being used anywhere (in addition to the minibuffer)?
lyxserver can use it... I think it does not matter much, but we shall not remove it without removing all the rest and provide a backup plan to be able to change fonts via the minibuffer. JMarc