--- a/src/Pure/Admin/build_fonts.scala Mon Oct 04 13:32:34 2021 +0200
+++ b/src/Pure/Admin/build_fonts.scala Mon Oct 04 13:39:38 2021 +0200
@@ -57,6 +57,7 @@
0x2013, // dash
0x2014, // dash
0x2015, // dash
+ 0x2016, // big parallel
0x2020, // dagger
0x2021, // double dagger
0x2022, // bullet