src/Pure/library.scala
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  }