src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Thu Feb 13 14:10:50 2025 +0100
+++ b/src/Pure/General/url.scala	Thu Feb 13 14:16:11 2025 +0100
@@ -132,6 +132,12 @@
     else Some(s.substring(0, j + 1))
   }
 
+  def get_ext(str: String): String = {
+    val s = get_base_name(str).getOrElse("")
+    val i = s.lastIndexOf('.')
+    if (i < 0 || i + 1 >= s.length) "" else s.substring(i + 1)
+  }
+
   def append_path(prefix: String, suffix: String): String =
     if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.endsWith("\\") || prefix.isEmpty) {
       prefix + suffix