src/Tools/jEdit/src/jedit_options.scala

--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 23:04:53 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Aug 13 23:08:07 2022 +0200
@@ -54,7 +54,7 @@
   /* GUI components */
 
   class Bool_GUI(access: Bool_Access, label: String)
-  extends GUI.Bool(label, init = access()) {
+  extends GUI.Check(label, init = access()) {
     def load(): Unit = { selected = access() }
     override def clicked(state: Boolean): Unit = access.update(state)
   }