src/Pure/General/path.scala
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 =
   {