# HG changeset patch
# User wenzelm
# Date 1571051853 -7200
# Node ID 822f5cbfc5b6782b7be2b956d660413cb0381c6d
# Parent  545229df2f823acf4b4ff21593fc28cf25272a60
tuned signature;

diff -r 545229df2f82 -r 822f5cbfc5b6 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 12:07:37 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 13:17:33 2019 +0200
@@ -125,8 +125,17 @@
   {
     def session_dirs: List[Path] = dirs ::: select_dirs
 
+    def build_logic(logic: String)
+    {
+      Build.build_logic(options, logic, build_heap = true, progress = progress,
+        dirs = session_dirs, strict = true)
+    }
+
     def session(logic: String, log: Logger = No_Logger): Session =
+    {
+      build_logic(logic)
       new Session(this, logic, log)
+    }
   }
 
   class Session private[Dump](context: Context, logic: String, log: Logger)
@@ -135,9 +144,6 @@
 
     private val progress = context.progress
 
-    Build.build_logic(context.options, logic, build_heap = true, progress = progress,
-      dirs = context.session_dirs, strict = true)
-
     val resources: Headless.Resources =
       Headless.Resources.make(context.session_options, logic, progress = progress, log = log,
         session_dirs = context.session_dirs,