src/Pure/GUI/gui.scala
changeset 81674 70d2f72098df
parent 81670 3e51429404cd
child 82050 0f22f7b370b2
--- a/src/Pure/GUI/gui.scala	Fri Dec 27 18:01:34 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Dec 27 19:49:45 2024 +0100
@@ -102,8 +102,8 @@
         }
       }
 
-    def bullet: String = "\u2218"
-    def bullet_triangle: String = "\u25b9"
+    def regular_bullet: String = "\u2022"
+    def triangular_bullet: String = "\u2023"
   }
 
   abstract class Style_Symbol extends Style {