Hello, * Bruno Haible wrote on Sun, May 01, 2011 at 09:38:43PM CEST: > > Should we just play more with boldface output?
This sounds like an arms race again. Whenever that happens, it is usually most helpful in the long to consider removing output, or producing some of the other output more judiciously, not adding more and more noisy and shouting output. (Just a general observation, I don't have a particular suggestion here, and will go back to lurking and email catchup mode now.) Cheers, Ralf
