# HG changeset patch
# User wenzelm
# Date 1488897354 -3600
# Node ID c706b57b16942f9e6f5e0fe611f2e40752cca719
# Parent  1191df79aa1cc7d18cfce209641da007fcc7f3e1
clarified modules;

diff -r 1191df79aa1c -r c706b57b1694 etc/options
--- a/etc/options	Tue Mar 07 14:51:52 2017 +0100
+++ b/etc/options	Tue Mar 07 15:35:54 2017 +0100
@@ -193,6 +193,18 @@
   -- "limit for completion within the formal context"
 
 
+section "Spell Checker"
+
+public option spell_checker : bool = true
+  -- "enable spell-checker for prose words within document text, comments etc."
+
+public option spell_checker_dictionary : string = "en"
+  -- "spell-checker dictionary name"
+
+public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
+  -- "relevant markup elements for spell-checker, separated by commas"
+
+
 section "Secure Shell"
 
 option ssh_config_dir : string = "~/.ssh"
diff -r 1191df79aa1c -r c706b57b1694 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Mar 07 14:51:52 2017 +0100
+++ b/src/Tools/jEdit/etc/options	Tue Mar 07 15:35:54 2017 +0100
@@ -73,18 +73,6 @@
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
-section "Spell Checker"
-
-public option spell_checker : bool = true
-  -- "enable spell-checker for prose words within document text, comments etc."
-
-public option spell_checker_dictionary : string = "en"
-  -- "spell-checker dictionary name"
-
-public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
-  -- "relevant markup elements for spell-checker, separated by commas"
-
-
 section "Rendering of Document Content"
 
 option outdated_color : string = "EEE3E3FF"