src/Pure/Admin/build_fonts.scala
changeset 70066 6dc5506ad449
parent 69975 04c50000fad1
child 70253 9a03e9d5f336
     1.1 --- a/src/Pure/Admin/build_fonts.scala	Sat Mar 09 13:24:59 2019 +0100
     1.2 +++ b/src/Pure/Admin/build_fonts.scala	Sat Mar 09 13:35:49 2019 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4          0x203a,  // single guillemet
     1.5          0x204b,  // FOOTNOTE
     1.6          0x20ac,  // Euro
     1.7 +        0x2710,  // pencil
     1.8          0xfb01,  // ligature fi
     1.9          0xfb02,  // ligature fl
    1.10          0xfffd,  // replacement character