src/Pure/Tools/profiling.scala
changeset 79616 12bb31d01510
parent 79095 3bdd3cf5f5e0
child 79674 215db9299a1a
--- a/src/Pure/Tools/profiling.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Tools/profiling.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -225,7 +225,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1
+    max_jobs: Option[Int] = None
   ): Results = {
     /* sessions structure */
 
@@ -313,7 +313,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 options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
         var verbose = false
         var exclude_sessions: List[String] = Nil
@@ -345,7 +345,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))),
           "o:" -> (arg => options = options + arg),
           "v" -> (_ => verbose = true),
           "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))