equal
deleted
inserted
replaced
61 if Execution.running execution_id exec_id [group] then |
61 if Execution.running execution_id exec_id [group] then |
62 let |
62 let |
63 val res = |
63 val res = |
64 (body |
64 (body |
65 |> restore_attributes |
65 |> restore_attributes |
66 |> Future.worker_context "Command.memo_exec" group |
66 |> Future.task_context "Command.memo_exec" group |
67 |> Exn.interruptible_capture) (); |
67 |> Exn.interruptible_capture) (); |
68 in SOME ((), Result res) end |
68 in SOME ((), Result res) end |
69 else SOME ((), expr) |
69 else SOME ((), expr) |
70 end) () |
70 end) () |
71 | Result _ => SOME ((), expr))) |
71 | Result _ => SOME ((), expr))) |