--- a/src/Pure/System/options.scala Sat Mar 11 21:36:25 2023 +0100
+++ b/src/Pure/System/options.scala Mon Mar 13 10:51:10 2023 +0100
@@ -328,9 +328,6 @@
def update(name: String, x: String): Options = put(name, Options.String, x)
}
- def proper_string(name: String): Option[String] =
- Library.proper_string(string(name))
-
def seconds(name: String): Time = Time.seconds(real(name))
@@ -483,8 +480,5 @@
val string: Options.Access_Variable[String] =
new Options.Access_Variable[String](this, _.string)
- def proper_string(name: String): Option[String] =
- Library.proper_string(string(name))
-
def seconds(name: String): Time = value.seconds(name)
}