src/Pure/General/sql.scala
changeset 65741 cf42659364c9
parent 65740 83388f09e9ab
child 65748 1f4a80e80c88
--- a/src/Pure/General/sql.scala	Sat May 06 12:45:42 2017 +0200
+++ b/src/Pure/General/sql.scala	Sat May 06 12:52:29 2017 +0200
@@ -254,6 +254,9 @@
     }
     def date(column: Column): Date = stmt.db.date(res, column)
 
+    def timing(c1: Column, c2: Column, c3: Column) =
+      Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
+
     def get[A](column: Column, f: Column => A): Option[A] =
     {
       val x = f(column)