changeset 56333 | 38f1422ef473 |
parent 51662 | 3391a493f39a |
child 59149 | 0070053570c4 |
--- a/src/Pure/General/timing.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/General/timing.ML Mon Mar 31 10:28:08 2014 +0200 @@ -105,7 +105,7 @@ fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); fun protocol_message props t = - Output.try_protocol_message (props @ Markup.timing_properties t) ""; + Output.try_protocol_message (props @ Markup.timing_properties t) []; fun protocol props f x = let