NEWS
changeset 62254 81cbea2babd9
parent 62253 91363e4c196d
child 62284 1fd4831e9f93
--- 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 \<name> or \<^name> or \name is
 always possible, independently of the language context. It is never