redundant;
authorwenzelm
Wed, 17 Jul 2019 17:12:57 +0200
changeset 70373 2d337a2a561a
parent 70372 b5da5172d4e3
child 70374 2b4c40722f0b
redundant;
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