diff -r 91363e4c196d -r 81cbea2babd9 NEWS --- a/NEWS Sun Jan 31 19:54:40 2016 +0100 +++ b/NEWS Mon Feb 01 14:10:07 2016 +0100 @@ -90,8 +90,8 @@ due to ad-hoc updates by auxiliary GUI components, such as the State panel. -* Improved scheduling for urgent print tasks (e.g. command state output, -interactive queries) wrt. long-running background tasks. +* Slightly improved scheduling for urgent print tasks (e.g. command +state output, interactive queries) wrt. long-running background tasks. * Completion of symbols via prefix of \ or \<^name> or \name is always possible, independently of the language context. It is never