src/Pure/Thy/sessions.scala
changeset 69074 787f3db8e313
parent 69026 6e2f9f62aafd
child 69080 0f1cc8df3409
equal deleted inserted replaced
69073:d05defa39e3d 69074:787f3db8e313
  1106             password = options.string("build_database_password"),
  1106             password = options.string("build_database_password"),
  1107             database = options.string("build_database_name"),
  1107             database = options.string("build_database_name"),
  1108             host = options.string("build_database_host"),
  1108             host = options.string("build_database_host"),
  1109             port = options.int("build_database_port"),
  1109             port = options.int("build_database_port"),
  1110             ssh =
  1110             ssh =
  1111               proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
  1111               options.proper_string("build_database_ssh_host").map(ssh_host =>
  1112                 SSH.open_session(options,
  1112                 SSH.open_session(options,
  1113                   host = ssh_host,
  1113                   host = ssh_host,
  1114                   user = options.string("build_database_ssh_user"),
  1114                   user = options.string("build_database_ssh_user"),
  1115                   port = options.int("build_database_ssh_port"))),
  1115                   port = options.int("build_database_ssh_port"))),
  1116             ssh_close = true)
  1116             ssh_close = true)