tuned signature;

--- 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)
   }