tuned signature;
authorwenzelm
Sat, 13 Aug 2022 15:09:10 +0200
changeset 75843 d750ead045a1
parent 75842 a8c401312f9d
child 75844 7d27944d7141
tuned signature;
src/Pure/System/options.scala
--- 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)
   }