src/Pure/Tools/dump.scala
changeset 71726 a5fda30edae2
parent 71678 6fff34b5293e
child 71807 cdfa8f027bb9
--- a/src/Pure/Tools/dump.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -94,7 +94,7 @@
     def apply(
       options: Options,
       aspects: List[Aspect] = Nil,
-      progress: Progress = No_Progress,
+      progress: Progress = new Progress,
       dirs: List[Path] = Nil,
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty,
@@ -395,7 +395,7 @@
     options: Options,
     logic: String,
     aspects: List[Aspect] = Nil,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,