changeset 73571 | f86661e32bed |
parent 73565 | 1aa92bc4d356 |
child 73576 | b50f8cc8c08e |
--- a/src/Pure/System/scala.scala Mon Apr 12 22:18:37 2021 +0200 +++ b/src/Pure/System/scala.scala Mon Apr 12 22:26:09 2021 +0200 @@ -39,10 +39,7 @@ { override def multi: Boolean = false override def apply(args: List[String]): List[String] = - args match { - case List(arg) => List(apply(arg)) - case _ => error("Expected single argument for Scala function " + quote(name)) - } + List(apply(Library.the_single(args))) def apply(arg: String): String }