--- a/src/Pure/Tools/build_doc.scala Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/Tools/build_doc.scala Tue Sep 29 13:54:04 2015 +0200
@@ -16,7 +16,7 @@
def build_doc(
options: Options,
- progress: Build.Progress = Build.Ignore_Progress,
+ progress: Progress = Ignore_Progress,
all_docs: Boolean = false,
max_jobs: Int = 1,
system_mode: Boolean = false,
@@ -79,7 +79,7 @@
Properties.Value.Boolean(system_mode) ::
Command_Line.Chunks(docs) =>
val options = Options.init()
- val progress = new Build.Console_Progress()
+ val progress = new Console_Progress()
progress.interrupt_handler {
build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
}