# HG changeset patch
# User wenzelm
# Date 1708337228 -3600
# Node ID 82038b9eb89ad7308a074d5eda940f2aaaa8fdc0
# Parent  215db9299a1a6c320835cc6b7f736c95dfd4eb46
tuned;

diff -r 215db9299a1a -r 82038b9eb89a src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Sun Feb 18 19:09:05 2024 +0100
+++ b/src/Pure/Build/export.scala	Mon Feb 19 11:07:08 2024 +0100
@@ -674,8 +674,7 @@
 
         /* export files */
 
-        val store = Store(options)
-        export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
-          export_list = export_list, export_patterns = export_patterns)
+        export_files(Store(options), session_name, export_dir, progress = progress,
+          export_prune = export_prune, export_list = export_list, export_patterns = export_patterns)
       })
 }