author | wenzelm |
Wed, 17 Jul 2019 17:12:57 +0200 | |
changeset 70373 | 2d337a2a561a |
parent 70372 | b5da5172d4e3 |
child 70374 | 2b4c40722f0b |
--- a/src/Pure/Admin/build_fonts.scala Wed Jul 17 17:03:50 2019 +0200 +++ b/src/Pure/Admin/build_fonts.scala Wed Jul 17 17:12:57 2019 +0200 @@ -31,7 +31,6 @@ 0x204b, // FOOTNOTE 0x20ac, // Euro 0x2710, // pencil - 0x2aff, // n-ary Dijkstra choice 0xfb01, // ligature fi 0xfb02, // ligature fl 0xfffd, // replacement character