--- a/src/Pure/Tools/build_process.scala Sun Feb 26 18:52:33 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sun Feb 26 19:14:47 2023 +0100
@@ -443,8 +443,6 @@
}
def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit = {
- db.using_statement(
- State.table.delete() + SQL.where(Generic.sql_equal(instance = instance)))(_.execute())
db.using_statement(State.table.insert()) { stmt =>
stmt.string(1) = instance
stmt.long(2) = serial
@@ -453,6 +451,10 @@
}
}
+ def reset_state(db: SQL.Database, instance: String): Unit =
+ db.using_statement(
+ State.table.delete() + SQL.where(Generic.sql_equal(instance = instance)))(_.execute())
+
def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
val tables =
List(Config.table, State.table, Pending.table, Running.table, Results.table)
@@ -478,7 +480,10 @@
val (serial0, numa_index0) = read_state(db, instance)
val serial = if (ch1 || ch2 || ch3) serial0 + 1 else serial0
- if (serial != serial0) write_state(db, instance, serial, state.numa_index)
+ if (serial != serial0) {
+ reset_state(db, instance)
+ write_state(db, instance, serial, state.numa_index)
+ }
state.copy(serial = serial)
}