changeset 77621 | 25993910f212 |
parent 77617 | 58b7f3fb73cb |
child 77624 | 809ad223f406 |
--- 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"),