src/Pure/ROOT.scala
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 _