tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
authorwenzelm
Mon, 01 Feb 2016 14:10:07 +0100
changeset 62254 81cbea2babd9
parent 62253 91363e4c196d
child 62255 f3736c02cb3f
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
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 \<name> or \<^name> or \name is
 always possible, independently of the language context. It is never