changeset 76351 | 2cee31cd92f0 |
parent 76136 | 1bb677cceea4 |
child 76365 | 24e951a8a318 |
--- a/src/Pure/Admin/build_history.scala Fri Oct 21 14:45:13 2022 +0200 +++ b/src/Pure/Admin/build_history.scala Fri Oct 21 16:39:31 2022 +0200 @@ -359,7 +359,7 @@ session_build_info ::: ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: session_errors.map(Protocol.Error_Message_Marker.apply) ::: - heap_sizes), XZ.options(6)) + heap_sizes), Compress.Options_XZ(6)) /* next build */