changeset 73340 | 0ffcad1f6130 |
parent 72897 | 86eff7a823f3 |
child 73512 | e52a9b208481 |
--- a/src/Pure/Admin/build_doc.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/Admin/build_doc.scala Mon Mar 01 22:22:12 2021 +0100 @@ -16,7 +16,7 @@ progress: Progress = new Progress, all_docs: Boolean = false, max_jobs: Int = 1, - docs: List[String] = Nil) + docs: List[String] = Nil): Unit = { val store = Sessions.store(options)