src/Pure/General/file.scala
changeset 76533 2590980401b0
parent 76529 ded37aade88e
child 76540 83de6e9ae983
--- a/src/Pure/General/file.scala	Fri Nov 25 16:20:14 2022 +0100
+++ b/src/Pure/General/file.scala	Fri Nov 25 20:17:54 2022 +0100
@@ -83,6 +83,7 @@
   def is_node(s: String): Boolean = s.endsWith(".node")
   def is_pdf(s: String): Boolean = s.endsWith(".pdf")
   def is_png(s: String): Boolean = s.endsWith(".png")
+  def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
   def is_thy(s: String): Boolean = s.endsWith(".thy")
   def is_xz(s: String): Boolean = s.endsWith(".xz")
   def is_zip(s: String): Boolean = s.endsWith(".zip")