tuned signature: removed unused arguments;
authorwenzelm
Mon, 21 Aug 2023 11:15:25 +0200
changeset 78546 e3ae7293c5df
parent 78545 5f4ca329fde4
child 78547 7f564f33172b
tuned signature: removed unused arguments;
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
           }
       }