author | wenzelm |
Fri, 07 Sep 2018 19:49:26 +0200 | |
changeset 68931 | fc5763d000e8 |
parent 68930 | 19ddfe546620 |
child 68932 | e609c3dec6f8 |
--- a/src/Pure/PIDE/command.ML Fri Sep 07 19:27:28 2018 +0200 +++ b/src/Pure/PIDE/command.ML Fri Sep 07 19:49:26 2018 +0200 @@ -452,7 +452,7 @@ fun run_process execution_id exec_id process = let val group = Future.worker_subgroup () in if Execution.running execution_id exec_id [group] then - ignore (task_context group Lazy.force_result {strict = true} process) + ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) else () end;