# HG changeset patch
# User wenzelm
# Date 1670341955 -3600
# Node ID c9f89707708993494100e4b427f6e0fd12aee5a9
# Parent  71942a6af4eda03412cd55c2cad220811943e840
tuned;

diff -r 71942a6af4ed -r c9f897077089 src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Dec 06 16:44:47 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Dec 06 16:52:35 2022 +0100
@@ -92,10 +92,7 @@
       override val title: String = opt.title_jedit
       override def load(): Unit = {
         val lang = PIDE.options.string(option_name)
-        Spell_Checker.get_dictionary(lang) match {
-          case Some(dict) => selection.item = GUI.Selector.item(dict)
-          case None =>
-        }
+        for (dict <- Spell_Checker.get_dictionary(lang)) selection.item = GUI.Selector.item(dict)
       }
       override def save(): Unit =
         for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang