changeset 62826 | eb94e570c1a4 |
parent 62505 | 9e2a65912111 |
child 62895 | 54c2abe7e9a4 |
--- a/src/Pure/PIDE/command.ML Sat Apr 02 23:14:08 2016 +0200 +++ b/src/Pure/PIDE/command.ML Sat Apr 02 23:29:05 2016 +0200 @@ -417,7 +417,7 @@ in (case delay of NONE => fork () - | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork)) + | SOME d => ignore (Event_Timer.request (Time.now () + d) fork)) end else run_process execution_id exec_id print_process;