--- a/src/Pure/ROOT.scala Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/ROOT.scala Mon Dec 03 14:59:42 2018 +0100
@@ -10,7 +10,7 @@
val error = Exn.error _
def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
- def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f)
+ def using[A <: AutoCloseable, B](a: A)(f: A => B): B = Library.using(a)(f)
val space_explode = Library.space_explode _
val split_lines = Library.split_lines _
val cat_lines = Library.cat_lines _
@@ -25,4 +25,3 @@
type UUID = java.util.UUID
def UUID(): UUID = java.util.UUID.randomUUID()
}
-