changeset 75843 | d750ead045a1 |
parent 75842 | a8c401312f9d |
child 75844 | 7d27944d7141 |
--- a/src/Pure/System/options.scala Sat Aug 13 15:06:23 2022 +0200 +++ b/src/Pure/System/options.scala Sat Aug 13 15:09:10 2022 +0200 @@ -243,7 +243,7 @@ /* basic operations */ - private def put[A](name: String, typ: Options.Type, value: String): Options = { + private def put(name: String, typ: Options.Type, value: String): Options = { val opt = check_type(name, typ) new Options(options + (name -> opt.copy(value = value)), section) }