# HG changeset patch
# User wenzelm
# Date 1708265780 -3600
# Node ID 26fa2e8761fb517cc9e213563b18075de571bebc
# Parent  4a299bdb5d61967e4fdd46cdce0874508101a23a
minor performance tuning;

diff -r 4a299bdb5d61 -r 26fa2e8761fb src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sun Feb 18 15:15:07 2024 +0100
+++ b/src/Pure/Build/store.scala	Sun Feb 18 15:16:20 2024 +0100
@@ -279,8 +279,8 @@
   /* session */
 
   def get_session(name: String): Store.Session = {
-    val heap = input_dirs.map(_ + store.heap(name)).find(_.is_file)
-    val log_db = input_dirs.map(_ + store.log_db(name)).find(_.is_file)
+    val heap = input_dirs.view.map(_ + store.heap(name)).find(_.is_file)
+    val log_db = input_dirs.view.map(_ + store.log_db(name)).find(_.is_file)
     Store.Session(name, heap, log_db)
   }