# HG changeset patch
# User wenzelm
# Date 1688320263 -7200
# Node ID eca6ae2a09d7017045ee7ec33f38f5e8f571213f
# Parent  635ba0cbfe60e71b9a64fbc96e78722d2cc7fb31
removed junk;

diff -r 635ba0cbfe60 -r eca6ae2a09d7 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Jul 02 19:12:29 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 19:51:03 2023 +0200
@@ -550,8 +550,6 @@
       serial: Long,
       stop: Boolean = false
     ): Unit = {
-      val sql =
-
       db.execute_statement(
         Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
           sql = Workers.worker_uuid.where_equal(worker_uuid)),