changeset 82742 | 085e624a1303 |
parent 82720 | 956ecf2c07a0 |
child 82752 | 20ffc02d0b0e |
--- a/src/Pure/Build/build_schedule.scala Mon Jun 23 14:10:59 2025 +0200 +++ b/src/Pure/Build/build_schedule.scala Mon Jun 23 14:42:40 2025 +0200 @@ -1490,7 +1490,7 @@ numa_shuffling: Boolean = false, augment_options: String => List[Options.Spec] = _ => Nil, session_setup: (String, Session) => Unit = (_, _) => (), - cache: Term.Cache = Term.Cache.make() + cache: Rich_Text.Cache = Rich_Text.Cache.make() ): Schedule = { Build.build_process(options, build_cluster = true, remove_builds = true)