src/Pure/Admin/jenkins.scala

--- a/src/Pure/Admin/jenkins.scala	Fri Oct 21 14:45:13 2022 +0200
+++ b/src/Pure/Admin/jenkins.scala	Fri Oct 21 16:39:31 2022 +0200
@@ -112,7 +112,7 @@
         File.write_xz(log_path,
           terminate_lines(Url.read(main_log) ::
             ml_statistics.map(Protocol.ML_Statistics_Marker.apply)),
-          XZ.options(6))
+          Compress.Options_XZ(6))
       }
     }
   }