src/Pure/Build/build_schedule.scala
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)