src/Pure/General/http.scala
changeset 69366 b6dacf6eabe3
parent 69364 91dbade9a5fa
child 69374 ab66951166f3
--- a/src/Pure/General/http.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -161,11 +161,11 @@
       {
         val uri_name = arg.uri.toString
         if (uri_name == root) {
-          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.base_name))))
+          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
         }
         else {
           html_fonts.collectFirst(
-            { case entry if uri_name == root + "/" + entry.path.base_name => Response(entry.bytes) })
+            { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
         }
       })
 }