tuned;

--- a/src/Pure/General/url.scala	Sun Jan 21 14:05:14 2024 +0100
+++ b/src/Pure/General/url.scala	Sun Jan 21 14:12:14 2024 +0100
@@ -60,8 +60,7 @@
   /* file name */
 
   def file_name(url: Url): String =
-    Library.take_suffix[Char](c => c != '/' && c != '\\',
-      url.java_url.getFile.toString.toList)._2.mkString
+    Library.take_suffix[Char](c => c != '/' && c != '\\', url.java_url.getFile.toList)._2.mkString
 
   def trim_index(url: Url): Url = {
     Library.try_unprefix("/index.html", url.toString) match {