# HG changeset patch
# User wenzelm
# Date 1545926395 -3600
# Node ID 9457d85204f51aee773214be02e0969a0ee9262a
# Parent  0428fd0a13b7c750c608771458dbe435717038cb
unused;

diff -r 0428fd0a13b7 -r 9457d85204f5 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Dec 27 16:32:19 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Dec 27 16:59:55 2018 +0100
@@ -93,7 +93,6 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
-    verbose: Boolean = false,
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
   {
@@ -245,7 +244,6 @@
             dirs = dirs,
             select_dirs = select_dirs,
             output_dir = output_dir,
-            verbose = verbose,
             selection = Sessions.Selection(
               requirements = requirements,
               all_sessions = all_sessions,