src/HOL/Tools/Mirabelle/mirabelle.scala
changeset 79616 12bb31d01510
parent 77628 a538dab533ef
child 79819 141df3fb25bf
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -42,7 +42,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
   ): Build.Results = {
     require(!selection.requirements)
     Isabelle_System.make_directory(output_dir)
@@ -123,7 +123,7 @@
       var all_sessions = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
-      var max_jobs = 1
+      var max_jobs: Option[Int] = None
       var verbose = false
       var exclude_sessions: List[String] = Nil
 
@@ -174,7 +174,7 @@
         "a" -> (_ => all_sessions = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
         "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
         "o:" -> (arg => options = options + arg),
         "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),