# HG changeset patch
# User wenzelm
# Date 1688824377 -7200
# Node ID 555fb8c536b352f5ddb44114cf7b19461acce35b
# Parent  d8c99a497502c69c8dbea4b94606faa163623a24
tuned: avoid redundant db access;

diff -r d8c99a497502 -r 555fb8c536b3 src/Pure/Tools/build_process.scala
--- 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