changeset 64909 | 8007f10195af |
parent 64310 | 3584841f2d2c |
child 65082 | 2e99c0ee3bac |
--- a/src/Pure/Admin/build_doc.scala Mon Jan 16 21:33:09 2017 +0100 +++ b/src/Pure/Admin/build_doc.scala Mon Jan 16 21:53:44 2017 +0100 @@ -16,7 +16,7 @@ def build_doc( options: Options, - progress: Progress = Ignore_Progress, + progress: Progress = No_Progress, all_docs: Boolean = false, max_jobs: Int = 1, system_mode: Boolean = false,