# HG changeset patch
# User wenzelm
# Date 1528725028 -7200
# Node ID 33114721ac9a616a4fa0277b8322d6927edff47c
# Parent  d8363de2656744998f9f18ae35c1af1c90fcdd5a
tuned signature;

diff -r d8363de26567 -r 33114721ac9a src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Jun 11 08:15:43 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Jun 11 15:50:28 2018 +0200
@@ -78,6 +78,10 @@
 
   val default_output_dir = Path.explode("dump")
 
+  def make_options(options: Options, aspects: List[Aspect]): Options =
+    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
+      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+
   def dump(options: Options, logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
@@ -92,9 +96,7 @@
     if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
       system_mode = system_mode) != 0) error(logic + " FAILED")
 
-    val dump_options =
-      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
-        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+    val dump_options = make_options(options, aspects)
 
 
     /* dependencies */