src/Pure/Admin/jenkins.scala

--- a/src/Pure/Admin/jenkins.scala	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon Mar 30 11:59:44 2020 +0200
@@ -112,7 +112,7 @@
 
         File.write_xz(log_path,
           terminate_lines(Url.read(main_log) ::
-            ml_statistics.map(Build_Log.ML_Statistics_Marker.apply)),
+            ml_statistics.map(Protocol.ML_Statistics_Marker.apply)),
           XZ.options(6))
       }
     }