--- a/src/Pure/Tools/build_process.scala Sat Jul 08 13:13:10 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Sat Jul 08 15:52:57 2023 +0200
@@ -733,8 +733,12 @@
)
def update_results(db: SQL.Database, results: State.Results): Boolean = {
- val old_results = read_results_domain(db)
- val insert = results.valuesIterator.filterNot(res => old_results.contains(res.name)).toList
+ val insert =
+ if (results.isEmpty) Nil
+ else {
+ val old_results = read_results_domain(db)
+ results.valuesIterator.filterNot(res => old_results.contains(res.name)).toList
+ }
for (result <- insert) {
val process_result = result.process_result