changeset 71726 | a5fda30edae2 |
parent 69854 | cc0b3e177b49 |
child 71896 | ce06d6456cc8 |
--- a/src/Pure/Admin/build_doc.scala Tue Apr 07 21:07:28 2020 +0200 +++ b/src/Pure/Admin/build_doc.scala Tue Apr 07 21:49:36 2020 +0200 @@ -16,7 +16,7 @@ def build_doc( options: Options, - progress: Progress = No_Progress, + progress: Progress = new Progress, all_docs: Boolean = false, max_jobs: Int = 1, docs: List[String] = Nil): Int =