tuned: avoid redundant db access;
authorwenzelm
Sat, 08 Jul 2023 15:52:57 +0200
changeset 78267 555fb8c536b3
parent 78266 d8c99a497502
child 78268 4be047eaee2b
tuned: avoid redundant db access;
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