src/Pure/General/path.scala
changeset 75119 7bf685cbc789
parent 75107 7c0217c8b8a5
child 75220 1cbdf9cfc94b
--- a/src/Pure/General/path.scala	Mon Feb 21 20:31:30 2022 +0100
+++ b/src/Pure/General/path.scala	Mon Feb 21 20:50:01 2022 +0100
@@ -215,6 +215,7 @@
     }
   def is_java: Boolean = ends_with(".java")
   def is_scala: Boolean = ends_with(".scala")
+  def is_pdf: Boolean = ends_with(".pdf")
 
   def ext(e: String): Path =
     if (e == "") this