| 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