changeset 80270 | 1d4300506338 |
parent 80261 | e3f472221f8f |
child 80271 | 198fc882ec0f |
--- a/src/Pure/Build/build_manager.scala Thu Jun 06 21:13:51 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jun 06 21:48:36 2024 +0200 @@ -88,7 +88,7 @@ enum Priority { case low, normal, high } - sealed trait T extends Library.Named + sealed trait T extends Name.T sealed case class Task( build_config: Build_Config,