--- a/src/Pure/Build/store.scala Mon Jun 23 14:10:59 2025 +0200
+++ b/src/Pure/Build/store.scala Mon Jun 23 14:42:40 2025 +0200
@@ -14,7 +14,7 @@
def apply(
options: Options,
build_cluster: Boolean = false,
- cache: Term.Cache = Term.Cache.make()
+ cache: Rich_Text.Cache = Rich_Text.Cache.make()
): Store = new Store(options, build_cluster, cache)
@@ -277,7 +277,7 @@
class Store private(
val options: Options,
val build_cluster: Boolean,
- val cache: Term.Cache
+ val cache: Rich_Text.Cache
) {
store =>