src/Pure/General/timing.scala
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")