# HG changeset patch
# User wenzelm
# Date 1660396150 -7200
# Node ID d750ead045a1461dfb6f3487db19f5ed69abe6de
# Parent  a8c401312f9dbb32787f04685e322166ccacb60d
tuned signature;

diff -r a8c401312f9d -r d750ead045a1 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)
   }