src/Pure/library.scala
changeset 40848 8662b9b1f123
parent 40475 8a57ff2c2600
child 43442 e1fff67b23ac
--- a/src/Pure/library.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/library.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -137,12 +137,12 @@
 
   def timeit[A](message: String)(e: => A) =
   {
-    val start = System.nanoTime()
+    val start = System.currentTimeMillis()
     val result = Exn.capture(e)
-    val stop = System.nanoTime()
+    val stop = System.currentTimeMillis()
     System.err.println(
       (if (message == null || message.isEmpty) "" else message + ": ") +
-        ((stop - start).toDouble / 1000000) + "ms elapsed time")
+        new Time(stop - start).message + " elapsed time")
     Exn.release(result)
   }
 }