| Fri, 27 Aug 2010 20:28:58 +0200 | wenzelm | eliminated obsolete Output.no_warnings, where no warnings were produced anyway; | changeset | files |
| Fri, 27 Aug 2010 20:09:36 +0200 | wenzelm | eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; | changeset | files |
| Fri, 27 Aug 2010 19:43:28 +0200 | wenzelm | more careful treatment of context visibility flag wrt. spurious warnings; | changeset | files |