src/Pure/PIDE/command.ML
changeset 53976 da610b507799
parent 53709 84522727f9d3
child 54519 5fed81762406
child 54637 db3d3d99c69d
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Sep 29 00:15:05 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sun Sep 29 11:21:02 2013 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4  local
     1.5  
     1.6  fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
     1.7 -  if Multithreading.enabled () then
     1.8 +  if Multithreading.enabled () orelse pri <= 0 then
     1.9      let
    1.10        val group = Future.worker_subgroup ();
    1.11        fun fork () =