| changeset 83287 | 24000abcefab |
| parent 83262 | 9fe2fedc9842 |
| child 83295 | 094d96f05cba |
--- a/src/Pure/Build/build_job.scala Wed Oct 15 16:31:05 2025 +0200 +++ b/src/Pure/Build/build_job.scala Wed Oct 15 21:53:16 2025 +0200 @@ -219,12 +219,6 @@ nodes_changed += state_id nodes_delay.invoke() } - - def get_theory_timings(): List[Properties.T] = synchronized { - nodes_domain.map(name => - Markup.Name(name.theory) ::: - Markup.Timing_Properties(nodes_status(name).total_timing)) - } } class Session_Job private[Build_Job](