--- 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) })
}
})
}