changeset 46120 | b769a3a370ad |
parent 45831 | 640c2b957f16 |
child 46535 | ac6e704dcd12 |
1.1 --- a/src/Pure/library.scala Sat Oct 22 23:28:24 2011 +0200 1.2 +++ b/src/Pure/library.scala Sat Oct 22 23:29:11 2011 +0200 1.3 @@ -219,7 +219,7 @@ 1.4 val stop = System.currentTimeMillis() 1.5 System.err.println( 1.6 (if (message == null || message.isEmpty) "" else message + ": ") + 1.7 - new Time(stop - start).message + " elapsed time") 1.8 + Time.ms(stop - start).message + " elapsed time") 1.9 Exn.release(result) 1.10 } 1.11 }