# HG changeset patch
# User wenzelm
# Date 1397460522 -7200
# Node ID 1f9d706968c2d415814a2df7643cfb5313b222b3
# Parent  6e4f2d4215b019567f118e049f1d531c6d1534c9
tuned;

diff -r 6e4f2d4215b0 -r 1f9d706968c2 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Apr 14 09:24:47 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Apr 14 09:28:42 2014 +0200
@@ -54,7 +54,7 @@
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
-public option spell_checker_language : string = "en_US"
+public option spell_checker_dictionary : string = "en_US"
   -- "spell-checker dictionary name"
 
 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
diff -r 6e4f2d4215b0 -r 1f9d706968c2 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 09:24:47 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 09:28:42 2014 +0200
@@ -83,7 +83,7 @@
   {
     Swing_Thread.require()
 
-    val option_name = "spell_checker_language"
+    val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
     val entries = dictionaries()
@@ -175,7 +175,7 @@
 
   def update(options: Options): Unit = synchronized {
     if (options.bool("spell_checker")) {
-      val lang = options.string("spell_checker_language")
+      val lang = options.string("spell_checker_dictionary")
       if (current_spell_checker._1 != lang) {
         Spell_Checker.dictionaries.find(_.lang == lang) match {
           case Some(dictionary) =>