author | wenzelm |
Sun, 29 Sep 2013 11:21:02 +0200 | |
changeset 53976 | da610b507799 |
parent 53975 | 22ee3fb9d596 |
child 53977 | a7add756b9d2 |
--- 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 () =