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