proper file name instead of font name (amending dc9a39c3f75d);
authorwenzelm
Sun, 22 Sep 2019 19:04:11 +0200
changeset 70933 342b0a1fc86d
parent 70932 e21c6b677c79
child 70934 b605c9cf82a2
proper file name instead of font name (amending dc9a39c3f75d);
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