diff -r a01f4cf202fd -r 12bb31d01510 src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Thu Feb 15 10:32:36 2024 +0100 +++ b/src/Pure/Admin/build_doc.scala Thu Feb 15 11:33:36 2024 +0100 @@ -14,7 +14,7 @@ options: Options, progress: Progress = new Progress, all_docs: Boolean = false, - max_jobs: Int = 1, + max_jobs: Option[Int] = None, sequential: Boolean = false, docs: List[String] = Nil, view: Boolean = false @@ -85,7 +85,7 @@ { args => var view = false var all_docs = false - var max_jobs = 1 + var max_jobs: Option[Int] = None var sequential = false var options = Options.init() @@ -105,7 +105,7 @@ """, "V" -> (_ => view = true), "a" -> (_ => all_docs = true), - "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))), "o:" -> (arg => options = options + arg), "s" -> (_ => sequential = true))