# HG changeset patch
# User wenzelm
# Date 1380446462 -7200
# Node ID da610b50779991bda93d8d328164602d8b53437b
# Parent  22ee3fb9d596fee3569915cfe59fcee4eca473a3
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;

diff -r 22ee3fb9d596 -r da610b507799 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Sep 29 00:15:05 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Sep 29 11:21:02 2013 +0200
@@ -318,7 +318,7 @@
 local
 
 fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
-  if Multithreading.enabled () then
+  if Multithreading.enabled () orelse pri <= 0 then
     let
       val group = Future.worker_subgroup ();
       fun fork () =