--- a/src/Pure/Admin/build_log.scala Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/Admin/build_log.scala Sun May 13 16:37:36 2018 +0200
@@ -253,7 +253,7 @@
/* properties (YXML) */
- val xml_cache = new XML.Cache()
+ val xml_cache = XML.make_cache()
def parse_props(text: String): Properties.T =
try {
@@ -881,7 +881,7 @@
class Store private[Build_Log](options: Options)
{
- val xml_cache: XML.Cache = new XML.Cache()
+ val xml_cache: XML.Cache = XML.make_cache()
val xz_cache: XZ.Cache = XZ.make_cache()
def open_database(