diff -r 5f4ca329fde4 -r e3ae7293c5df src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Aug 21 10:55:30 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Mon Aug 21 11:15:25 2023 +0200 @@ -765,12 +765,7 @@ tables.filter(table => table.columns.exists(column => column.name == Generic.build_uuid.name)) - def pull_database( - db: SQL.Database, - worker_uuid: String, - hostname: String, - state: State - ): State = { + def pull_database(db: SQL.Database, worker_uuid: String, state: State): State = { val serial_db = read_serial(db) if (serial_db == state.serial) state else { @@ -787,13 +782,7 @@ } } - def update_database( - db: SQL.Database, - worker_uuid: String, - build_uuid: String, - hostname: String, - state: State - ): State = { + def update_database(db: SQL.Database, worker_uuid: String, state: State): State = { val changed = List( update_sessions(db, state.sessions), @@ -931,10 +920,9 @@ case None => body case Some(db) => Build_Process.private_data.transaction_lock(db, label = label) { - _state = Build_Process.private_data.pull_database(db, worker_uuid, hostname, _state) + _state = Build_Process.private_data.pull_database(db, worker_uuid, _state) val res = body - _state = - Build_Process.private_data.update_database(db, worker_uuid, build_uuid, hostname, _state) + _state = Build_Process.private_data.update_database(db, worker_uuid, _state) res } }