| changeset 80270 | 1d4300506338 |
| parent 80261 | e3f472221f8f |
| child 80271 | 198fc882ec0f |
| 80269:0428c7ad25aa | 80270:1d4300506338 |
|---|---|
86 } |
86 } |
87 } |
87 } |
88 |
88 |
89 enum Priority { case low, normal, high } |
89 enum Priority { case low, normal, high } |
90 |
90 |
91 sealed trait T extends Library.Named |
91 sealed trait T extends Name.T |
92 |
92 |
93 sealed case class Task( |
93 sealed case class Task( |
94 build_config: Build_Config, |
94 build_config: Build_Config, |
95 id: UUID.T = UUID.random(), |
95 id: UUID.T = UUID.random(), |
96 submit_date: Date = Date.now(), |
96 submit_date: Date = Date.now(), |