# HG changeset patch
# User wenzelm
# Date 1596831820 -7200
# Node ID 4d8b3209dae3b45806baefe1d101fec5f8ac30c1
# Parent  7773ec172572e7c0f22d8a248aea3e114d5cab8a
cache props;

diff -r 7773ec172572 -r 4d8b3209dae3 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:19:32 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:23:40 2020 +0200
@@ -71,7 +71,8 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null && session.session_options.bool("ML_statistics")) {
-        session.runtime_statistics.post(Session.Runtime_Statistics(props))
+        val stats = Session.Runtime_Statistics(session.xml_cache.props(props))
+        session.runtime_statistics.post(stats)
       }
     }