changeset 68131 | 62a3294edda3 |
parent 67885 | 839a624aabb9 |
child 68144 | 7b995cd6d5d4 |
--- a/src/Pure/ROOT.scala Wed May 09 20:45:57 2018 +0200 +++ b/src/Pure/ROOT.scala Wed May 09 22:03:02 2018 +0200 @@ -8,7 +8,7 @@ { val ERROR = Exn.ERROR val error = Exn.error _ - val cat_error = Exn.cat_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) val space_explode = Library.space_explode _