| changeset 56782 | 433cf57550fa | 
| parent 56691 | ad5d7461b370 | 
| child 57912 | dd9550f84106 | 
--- a/src/Pure/General/timing.scala Tue Apr 29 13:29:05 2014 +0200 +++ b/src/Pure/General/timing.scala Tue Apr 29 13:32:13 2014 +0200 @@ -20,7 +20,7 @@ val timing = stop - start if (timing.is_relevant) - System.err.println( + Output.warning( (if (message == null || message.isEmpty) "" else message + ": ") + timing.message + " elapsed time")