| changeset 76348 | a15f16e8ad18 |
| parent 76017 | 9ca22009c2d0 |
| child 76831 | 72daee8a39ca |
--- a/src/Pure/General/path.scala Thu Oct 20 23:46:49 2022 +0200 +++ b/src/Pure/General/path.scala Fri Oct 21 11:08:01 2022 +0200 @@ -240,6 +240,7 @@ def orig: Path = ext("orig") def patch: Path = ext("patch") def shasum: Path = ext("shasum") + def zst: Path = ext("zst") def backup: Path = { val (prfx, s) = split_path