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