# HG changeset patch
# User wenzelm
# Date 1678701070 -3600
# Node ID 25993910f21214de1063379ade51d6e975d38f8c
# Parent  58576816d3046b95573ec929d3df1157073342b4
tuned signature;

diff -r 58576816d304 -r 25993910f212 src/Pure/System/options.scala
--- 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)
 }
diff -r 58576816d304 -r 25993910f212 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Mar 11 21:36:25 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 13 10:51:10 2023 +0100
@@ -1486,7 +1486,7 @@
         host = options.string("build_database_host"),
         port = options.int("build_database_port"),
         ssh =
-          options.proper_string("build_database_ssh_host").map(ssh_host =>
+          proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
             SSH.open_session(options,
               host = ssh_host,
               user = options.string("build_database_ssh_user"),