changeset 57839 | d5b0fa6f1f7a |
parent 56944 | 578dc6b4be89 |
child 57844 | ae3eac418c5f |
--- a/src/Pure/PIDE/command.ML Fri Aug 01 15:08:49 2014 +0200 +++ b/src/Pure/PIDE/command.ML Fri Aug 01 22:52:53 2014 +0200 @@ -382,7 +382,7 @@ print_function "Execution.print" (fn {args, exec_id, ...} => if null args then - SOME {delay = NONE, pri = 1, persistent = false, strict = true, + SOME {delay = NONE, pri = 1, persistent = false, strict = false, print_fn = fn _ => fn _ => Execution.fork_prints exec_id} else NONE);