# HG changeset patch
# User wenzelm
# Date 1569171851 -7200
# Node ID 342b0a1fc86d4bf1d9ea4bfbc2ef781f5fefcfe5
# Parent  e21c6b677c79bc47b257ac96fc3f54ef2def103a
proper file name instead of font name (amending dc9a39c3f75d);

diff -r e21c6b677c79 -r 342b0a1fc86d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Sep 22 16:25:09 2019 +0200
+++ b/src/Pure/Thy/html.scala	Sun Sep 22 19:04:11 2019 +0200
@@ -351,7 +351,7 @@
 
   def fonts_url(): String => String =
     (for (entry <- Isabelle_Fonts.fonts(hidden = true))
-     yield (entry.name -> Url.print_file(entry.path.file))).toMap
+     yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap
 
   def fonts_dir(prefix: String)(ttf_name: String): String =
     prefix + "/" + ttf_name