changeset 78170 | c85eeff78b33 |
parent 78168 | 8fbe3b3d665b |
child 78172 | 43ed2541b758 |
--- a/src/Pure/Tools/build_process.scala Fri Jun 16 14:01:30 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Fri Jun 16 14:20:18 2023 +0200 @@ -848,9 +848,7 @@ _database match { case None => (build_progress, UUID.random().toString) case Some(db) => - val progress_db = - if (db.is_postgresql) store.open_database_server() - else db + val progress_db = store.open_build_database(Progress.Data.database) val progress = new Database_Progress(progress_db, build_progress, hostname = hostname,