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))