# HG changeset patch # User wenzelm # Date 1563376377 -7200 # Node ID 2d337a2a561a6d27100e891dc85d2c76f2c55b63 # Parent b5da5172d4e33ab0e5582c27c7ff16a91cea4f5d redundant; diff -r b5da5172d4e3 -r 2d337a2a561a src/Pure/Admin/build_fonts.scala --- 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