| changeset 50683 | 34b109c5324c |
| parent 50664 | fff984a77f58 |
| child 50909 | b2fb1ab1475d |
--- a/src/Pure/Concurrent/future.ML Wed Jan 02 13:20:10 2013 +0100 +++ b/src/Pure/Concurrent/future.ML Wed Jan 02 13:50:59 2013 +0100 @@ -204,7 +204,7 @@ ("workers_waiting", Markup.print_int waiting)] @ ML_Statistics.get (); in - Output.protocol_message (Markup.ML_statistics @ stats) "" + Output.protocol_message (Markup.ML_statistics :: stats) "" handle Fail msg => warning msg end else ();