src/Pure/Admin/build_fonts.scala
changeset 70371 3f9d03571eaa
parent 70369 6c65447b8a64
child 70373 2d337a2a561a
--- a/src/Pure/Admin/build_fonts.scala	Wed Jul 17 11:18:39 2019 +0200
+++ b/src/Pure/Admin/build_fonts.scala	Wed Jul 17 16:10:05 2019 +0200
@@ -97,6 +97,8 @@
         0x27e7,  // right white square bracket
         0x27e8,  // left angle bracket
         0x27e9,  // right angle bracket
+        0x27ea,  // left double angle bracket
+        0x27eb,  // right double angle bracket
       ) ++
       (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
       (0x2900 to 0x297f) ++  // Supplemental Arrows-B