author | wenzelm |
Sat, 25 Feb 2023 17:45:10 +0100 | |
changeset 77371 | 84ca5e036897 |
parent 77370 | 47c2ac81ddd4 |
child 77372 | 44fe9fe96130 |
--- a/src/Pure/Tools/build_job.scala Sat Feb 25 14:33:19 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Sat Feb 25 17:45:10 2023 +0100 @@ -22,7 +22,7 @@ } object Build_Job { - case class Abstract( + sealed case class Abstract( override val job_name: String, override val numa_node: Option[Int] ) extends Build_Job {