changeset 52600 | 75afb82daf5c |
parent 52599 | d7871f38ffb4 |
child 52602 | 00170ef1dc39 |
--- a/src/Pure/PIDE/document.ML Thu Jul 11 16:01:48 2013 +0200 +++ b/src/Pure/PIDE/document.ML Thu Jul 11 16:26:14 2013 +0200 @@ -334,7 +334,7 @@ (fn () => iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of - SOME exec => if running () then SOME (Command.execute exec) else NONE + SOME exec => if running () then SOME (Command.exec exec) else NONE | NONE => NONE)) node ())); in () end;