diff -r 157ad1f976d2 -r 809ad223f406 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon Mar 13 13:20:35 2023 +0100 +++ b/src/Pure/System/options.scala Mon Mar 13 13:43:25 2023 +0100 @@ -8,9 +8,9 @@ object Options { - type Spec = (String, Option[String]) + val empty: Options = new Options() - val empty: Options = new Options() + sealed case class Spec(name: String, value: Option[String] = None) sealed case class Change(name: String, value: String, unknown: Boolean) { def print_props: String = Properties.Eq(name, value) @@ -421,7 +421,7 @@ } def ++ (specs: List[Options.Spec]): Options = - specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) } + specs.foldLeft(this) { case (x, Options.Spec(y, z)) => x + (y, z) } /* sections */