1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jan 01 13:37:37 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jan 01 21:55:46 2013 +0100
     1.3 @@ -203,7 +203,10 @@
     1.4          ("workers_active", Markup.print_int active),
     1.5          ("workers_waiting", Markup.print_int waiting)] @
     1.6          ML_Statistics.get ();
     1.7 -    in Output.protocol_message (Markup.ML_statistics @ stats) "" end
     1.8 +    in
     1.9 +      Output.protocol_message (Markup.ML_statistics @ stats) ""
    1.10 +        handle Fail msg => warning msg
    1.11 +    end
    1.12    else ();
    1.13  
    1.14