changeset 73628 | ac8feb094bd4 |
parent 73522 | b219774a71ae |
child 73660 | ff716ecb0805 |
--- a/src/Pure/General/path.scala Wed May 05 13:27:30 2021 +0200 +++ b/src/Pure/General/path.scala Wed May 05 13:30:11 2021 +0200 @@ -217,6 +217,8 @@ def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") + def tar: Path = ext("tar") + def gz: Path = ext("gz") def backup: Path = {