# 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