src/Pure/Admin/build_log.scala
changeset 73025 3e5a61d9f46a
parent 73024 337e1b135d2f
child 73031 f93f0597f4fb
equal deleted inserted replaced
73024:337e1b135d2f 73025:3e5a61d9f46a
   872     {
   872     {
   873       PostgreSQL.open_database(
   873       PostgreSQL.open_database(
   874         user = user, password = password, database = database, host = host, port = port,
   874         user = user, password = password, database = database, host = host, port = port,
   875         ssh =
   875         ssh =
   876           if (ssh_host == "") None
   876           if (ssh_host == "") None
   877           else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)),
   877           else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
   878         ssh_close = true)
   878         ssh_close = true)
   879     }
   879     }
   880 
   880 
   881     def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
   881     def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
   882     {
   882     {