recovered missing glyph;
authorwenzelm
Sun Feb 10 18:12:24 2019 +0100 (5 months ago ago)
changeset 6997504c50000fad1
parent 69974 4791988fcbc4
child 69976 7e5a7a11d5d1
recovered missing glyph;
src/Pure/Admin/build_fonts.scala
     1.1 --- a/src/Pure/Admin/build_fonts.scala	Sun Feb 10 18:04:48 2019 +0100
     1.2 +++ b/src/Pure/Admin/build_fonts.scala	Sun Feb 10 18:12:24 2019 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4        (0x0400 to 0x04ff) ++  // Cyrillic
     1.5        (0x0600 to 0x06ff) ++  // Arabic
     1.6        Seq(
     1.7 +        0x02dd,  // hungarumlaut
     1.8          0x2018,  // single quote
     1.9          0x2019,  // single quote
    1.10          0x201a,  // single quote