src/Tools/jEdit/src/jedit_options.scala

--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Nov 08 13:00:24 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Nov 08 13:14:59 2023 +0100
@@ -186,7 +186,7 @@
           }
         text_area.peer.setInputVerifier({
             case text: JTextComponent =>
-              try { value + Options.Spec(opt_name, Some(text.getText)); true }
+              try { value + Options.Spec.eq(opt_name, text.getText); true }
               catch { case ERROR(_) => false }
             case _ => true
           })