diff -r a01f4cf202fd -r 12bb31d01510 src/Pure/Tools/profiling.scala --- 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)))