# HG changeset patch
# User wenzelm
# Date 1549818744 -3600
# Node ID 04c50000fad1670acb82a4ce7ab9b91e51384cb8
# Parent  4791988fcbc4917163830eb3f4393a40fae707f0
recovered missing glyph;

diff -r 4791988fcbc4 -r 04c50000fad1 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Sun Feb 10 18:04:48 2019 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Sun Feb 10 18:12:24 2019 +0100
@@ -19,6 +19,7 @@
       (0x0400 to 0x04ff) ++  // Cyrillic
       (0x0600 to 0x06ff) ++  // Arabic
       Seq(
+        0x02dd,  // hungarumlaut
         0x2018,  // single quote
         0x2019,  // single quote
         0x201a,  // single quote